proposition: Theorem mul_div_le : ∀ a b, b ≠ 0 → b ≠ ∞ → b * (a / b) ≤ a.
proof: Proof. intros a b Hb Hbi. destruct a as [a| ]; [ idtac | constructor ]. destruct b as [b| ]; [ simpl | exfalso; apply Hbi; reflexivity ]. apply le_fin. apply Nat.mul_div_le. intros H; apply Hb. subst b; reflexivity. Qed.
imports: Utf8 Compare_dec NPeano Misc