proposition: Lemma mod_mul : forall a b, 0<=a -> 0<b -> (a*b) mod b == 0.
proof: Proof. intros a b ? ?; symmetry. apply mod_unique with a; try split; try order. - apply mul_nonneg_nonneg; order. - nzsimpl; apply mul_comm. Qed.
imports: NZAxioms NZMulOrder