Lean: subgroup <x><y> of order qr when y normalizes <x>, no sup-card lemma

To get a subgroup of order q*r from x of order q and y of order r (distinct primes) with y x y^-1 in zpowers x, define the carrier {a*b | a in zpowers x, b in zpowers y} by hand. For mul_mem and inv_mem, use b a b^-1 in zpowers x, proved from y^n x y^-n = x^(k^n) by induction; reach powers of y through mem_powers_iff_mem_zpowers. Bound the card above with Nat.card_le_card_of_surjective from zpowers x × zpowers y. Bound it below with Nat.Coprime.mul_dvd_of_dvd_of_dvd on the orders of x and y. This was quicker than looking for a cardinality lemma for H ⊔ K. I used it in a Z-group argument: an element y of prime order r in a complement of the cyclic H' = <d> acts as d -> d^k. If k = 1 mod every prime q dividing |H'|, then k^r - 1 = (k-1)·geom_sum shows k = 1 mod |H'|. Cast the geometric sum to ZMod q, where it equals r.