proposition: Lemma coPrime1 : forall a : nat, CoPrime 1 a.
proof: Proof. split. - simpl. exists 1%Z. auto. - exists (Z.of_nat a); lia. - intros e [H H0] [H1 H2]. simpl in H0. symmetry in H0. assert (H >= 0 \/ H <= 0)%Z by lia. destruct H3. + pose proof (Zmult_one _ _ H3 H0). subst. exists 1%Z. lia. + assert (- H >= 0)%Z by lia. replace (H * e)%Z with ((- H) * (- e))%Z in H0 by lia. pose proof (Zmult_one _ _ H4 H0). rewrite H5 in H0. exists (-1)%Z. lia. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow