proposition: Lemma coPrimePrime : forall a b : nat, (forall p : nat, Prime p -> ~ divide p a \/ ~ divide p b) -> CoPrime a b.
proof: Proof. intros. unfold CoPrime. constructor. + exists (Z.of_nat a). lia. + exists (Z.of_nat b). lia. + intros. apply Zdivide_Zabs_inv_l in H0. apply Zdivide_Zabs_inv_l in H1. assert (Z.abs x = 0 \/ Z.abs x = 1 \/ 1 < Z.abs x)%Z by lia. destruct H2 as [H2 | [H2 | H2]]. - destruct H0. rewrite H2 in H0. destruct H1. rewrite H2 in H1. assert (a = 0) by lia. assert (b = 0) by lia. subst. assert (Prime 2). { apply prime_Prime. simpl. apply prime_2. } pose proof (H _ H3). destruct H4. * elim H4. exists 0. auto. * elim H4. exists 0. auto. - assert (x < 0 \/ 0 <= x)%Z by lia. destruct H3. * exists (-1)%Z. lia. * exists 1%Z. lia. - assert (1 < Z.to_nat (Z.abs x)) by lia. apply primeDiv in H3. destruct H3 as [p [H3 H4]]. pose proof (H _ H3). exfalso. destruct H4. destruct H5. * apply H5. destruct H0. exists (x0 * Z.to_nat x1). nia. * apply H5. destruct H1. exists (x0 * Z.to_nat x1). nia. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow