proposition: Lemma mul_div_le : forall a b, 0<=a -> 0<b -> b*(a/b) <= a.
proof: Proof. intros a b ? ?. rewrite (add_le_mono_r _ _ (a mod b)), <- div_mod by order. rewrite <- (add_0_r a) at 1. rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order. Qed.
imports: NZAxioms NZMulOrder