proposition: Theorem Ngauss_prime : forall a b c, (a | b * c) -> Nprime a -> (a | c) \/ (a | b).
proof: Proof. intros. destruct a. apply Nnot_prime_0 in H0. contradiction. assert(Ndiv_algo (S(a)) b=true -> ((S(a))|b)). intro. apply Ndiv_algo_complete. auto. auto with arith. auto. assert(Ndiv_algo (S a) b=false -> Nrel_prime (S a) b). intro. assert(~(S a|b)). intro. apply Ndiv_algo_correct in H3. rewrite H3 in H2. inversion H2. auto with arith. intro. intros. destruct n. destruct H4. rewrite Nat.mul_0_r in H4. inversion H4. destruct n. auto. destruct H0. apply H6 in H4. contradiction. split. auto with arith. apply Ndiv_le in H4. apply le_le_S_eq in H4. destruct H4. auto. rewrite H4 in H5. apply H3 in H5. contradiction. auto with arith. destruct (Ndiv_algo (S a) b). right. apply H1. auto. left. apply Ngauss with b. apply H. apply H2. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)