proposition: Theorem ZdividesDiv : forall n m p : Z, p <> 0%Z -> Zdivides (p * n) (p * m) -> Zdivides n m.
proof: Proof. intros n m p H' H'0. case H'0; intros q E. exists q. apply Zeq_mult_simpl with (c := p); auto. rewrite (Zmult_comm n); rewrite E; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz