proposition: Lemma div_pos: forall a b, 0<=a -> 0<b -> 0 <= a/b.
proof: Proof. intros a b ? ?. rewrite (mul_le_mono_pos_l _ _ b); auto; nzsimpl. rewrite (add_le_mono_r _ _ (a mod b)). rewrite <- div_mod by order. nzsimpl. apply mod_le; auto. Qed.
imports: NZAxioms NZMulOrder