proposition: Lemma squarec_spec : forall x, Φ(x *c x) = φ x * φ x.
proof: Proof. Proof (fun x => mulc_WW_spec x x). Lemma diveucl_spec_aux : forall a b, 0 < φ b -> let (q,r) := diveucl a b in φ a = φ q * φ b + φ r /\ 0 <= φ r < φ b. Proof. intros a b H;assert (W:= diveucl_spec a b). assert (φ b>0) by (auto with zarith). generalize (Z_div_mod φ a φ b H0). destruct (diveucl a b);destruct (Z.div_eucl φ a φ b). inversion W;rewrite Zmult_comm;trivial. Qed.
imports: CyclicAxioms ZArith Uint63