proposition: Theorem Zdiv_mult_le: forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b.
proof: Proof. intros a b c ? ? ?. zero_or_not b. apply Z.div_mul_le; auto. apply Z.le_neq; auto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms