proposition: Lemma div2_phi ih il j: (2^62 <= φ j -> φ ih < φ j -> φ (fst (diveucl_21 ih il j)) = Φ (WW ih il) / φ j)%Z.
proof: Proof. intros Hj Hj1. generalize (diveucl_21_spec_aux ih il j Hj Hj1). case diveucl_21; intros q r (Hq, Hr). apply Zdiv_unique with φ r; auto with zarith. simpl @fst; apply eq_trans with (1 := Hq); ring. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63