proposition: Lemma to_Z_gcd : forall i j, φ (gcd i j) = Zgcdn (2 * size) (φ j) (φ i).
proof: Proof. unfold gcd. elim (2*size)%nat. - reflexivity. - intros n ih i j; simpl. pose proof (to_Z_bounded j) as hj; pose proof (to_Z_bounded i). case eqbP; rewrite to_Z_0. + intros ->; rewrite Z.abs_eq; lia. + intros hne; rewrite ih; clear ih. rewrite <- mod_spec. revert hj hne; case φ j ; intros; lia. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63