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