proposition: Lemma gcd_spec a b : Zis_gcd (φ a) (φ b) (φ (gcd a b)).
proof: Proof. rewrite to_Z_gcd. apply Zis_gcd_sym. apply Zgcdn_is_gcd. unfold Zgcd_bound. generalize (to_Z_bounded b). destruct φ b as [|p|p]. - unfold size; auto with zarith. - intros (_,H). cut (Psize p <= size)%nat; [ lia | rewrite <- Zpower2_Psize; auto]. - intros (H,_); compute in H; elim H; auto. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63