proposition: Theorem Ngauss : forall a b c, (a | b * c) -> Nrel_prime a b -> (a | c).
proof: Proof. apply (nat_strong_ind (fun a => forall b c, (a|b*c) -> Nrel_prime a b -> (a|c))). intros. destruct H. rewrite Nat.mul_0_r in H. apply Nat.eq_mul_0 in H. destruct H. rewrite H in H0. apply Nnon_rel_prime_n_n in H0. contradiction. auto with arith. rewrite H. apply Ndiv_0. intros. destruct n. apply Ndiv_1. destruct H0. assert (diveucl b (S (S n))). apply eucl_dev. auto with arith. destruct H2. assert (diveucl c (S(S n))). apply eucl_dev. auto with arith. destruct H2. rewrite e in H0. rewrite e0 in H0. rewrite Nat.mul_add_distr_l in H0. rewrite Nat.mul_add_distr_r in H0. rewrite Nat.mul_add_distr_r in H0. assert (S (S n)|r*r0). apply Ndiv_plus_simpl with (q0 *S( S n) * r0). apply Ndiv_plus_simpl with (r * (q1 * S(S n))). apply Ndiv_plus_simpl with (q0 * S(S n) * (q1 * S(S n))). apply Ndivide_intro with q. rewrite <- H0. ring. apply Ndivide_intro with (q0*S(S n)*q1). ring. apply Ndivide_intro with (r*q1). ring. apply Ndivide_intro with (r0*q0). ring. destruct H2. assert (Nrel_prime (S(S n)) r). apply Nrel_prime_mod with b. auto. apply Nmod_intro with q0. auto. auto. assert (r|q2). apply H with (S(S n)). auto with arith. apply Ndivide_intro with r0. rewrite Nat.mul_comm. rewrite <- H2. ring. apply Nrel_prime_sym. auto. assert (S(S n)*r | r*r0). rewrite H2. rewrite Nat.mul_comm. apply Ndiv_strong_mult_compat. auto. assert (S(S n)|r0). apply Ndiv_mult_simpl with r. destruct r. rewrite Nat.add_0_r in e. assert (S(S n)|b). apply Ndivide_intro with q0. auto. assert (S(S n)=1). apply H1. apply Ndiv_n_n. auto. discriminate H7. auto with arith. destruct H5. apply Ndivide_intro with q3. rewrite Nat.mul_comm. rewrite H5. ring. rewrite e0. apply Ndiv_plus_compat. rewrite Nat.mul_comm. apply Ndiv_mult_compat. apply Ndiv_n_n. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)