proposition: Lemma coPrimeMult : forall a b c : nat, CoPrime a b -> divide a (b * c) -> divide a c.
proof: Proof. intros ? ? ? H H0; unfold CoPrime in H. destruct a as [| a]. - induction H0 as (x, H0). cbn in H0; rewrite Nat.eq_mul_0 in H0. destruct H0 as [H1 | H1]. + rewrite H1 in H; simpl in H. inversion H. clear H H0 H1 H2. assert (2 | 0). { exists 0%Z. auto. } destruct (H3 _ H H). nia. + rewrite H1; now exists 0%nat. - assert (H1: (S a > 0)%nat) by apply Nat.lt_0_succ. pose (gcd_bezout_nat (S a) b 1 H1 H) as W. inversion W; clear W; destruct H0 as [x1 H0]. assert (1 * Z.of_nat c = Z_of_nat (S a) * (u * Z.of_nat c + Z.of_nat x1 * v))%Z. { rewrite (Z.mul_comm (Z.of_nat (S a))). rewrite Z.mul_add_distr_r. rewrite (Z.mul_comm (u * Z.of_nat c)). rewrite (Z.mul_comm (Z.of_nat x1 * v)). repeat rewrite Z.mul_assoc. rewrite <- Znat.inj_mult. rewrite <- H0. rewrite Znat.inj_mult. rewrite (Z.mul_comm (Z.of_nat b)). rewrite <- (Z.mul_assoc (Z.of_nat c)). rewrite (Z.mul_comm (Z.of_nat c)). rewrite <- Z.mul_add_distr_r. nia. } rewrite Zmult_1_l in H3. assert (Z.divide (Z.of_nat (S a)) (Z.of_nat c)). { exists (u * Z.of_nat c + Z.of_nat x1 * v)%Z. now rewrite Z.mul_comm at 1. } clear H2 H3 u v. rewrite <- (Znat.Zabs2Nat.id (S a)). rewrite <- (Znat.Zabs2Nat.id c). repeat rewrite Zabs2Nat.id. destruct H4. exists (Z.to_nat x). nia. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow