proposition: Theorem ZdividesMult : forall n m p : Z, Zdivides n m -> Zdivides (p * n) (p * m).
proof: Proof. intros n m p H'; red in H'. elim H'; intros q E. red in |- *. exists q. rewrite E. auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz