proposition: Lemma mul_div_le : forall a b, 0<b -> b*(a/b) <= a.
proof: Proof. intros a b **. rewrite (div_mod a b) at 2; try order. rewrite <- (add_0_r (b*(a/b))) at 1. rewrite <- add_le_mono_l. now destruct (mod_pos_bound a b). Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv