proposition: Lemma mod_divides : forall a b, 0<=a -> 0<b -> (a mod b == 0 <-> exists c, a == b*c).
proof: Proof. intros a b ? ?; split. - intros. exists (a/b). rewrite div_exact; auto. - intros (c,Hc). rewrite Hc, mul_comm. apply mod_mul; auto. rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order. Qed.
imports: NZAxioms NZMulOrder