proposition: Lemma mod_mult_0 : forall (p : nat) (a b : Z), Prime p -> Mod (a * b) 0 p -> Mod a 0 p \/ Mod b 0 p.
proof: Proof. intros. elim (moddivmin (a * b) 0 p). intros. rewrite <- Zminus_0_l_reverse in H1. rewrite abs_mult in H1. elim (primedivmult p (Z.abs_nat a) (Z.abs_nat b)). left. elim (moddivmin a 0 p). intros. apply H5. rewrite <- Zminus_0_l_reverse. assumption. right. elim (moddivmin b 0 p). intros. apply H5. rewrite <- Zminus_0_l_reverse. assumption. assumption. apply H1. assumption. Qed.
imports: Arith ZArith Wf_nat lemmas natZ dec list exp divides prime modulo gcd