proposition: Theorem div_mul : ∀ a b, b ≠ 0 → b ≠ ∞ → a * b / b = a.
proof: Proof. intros a b Hb Hbi. destruct b as [b| ]; [ idtac | exfalso; apply Hbi; reflexivity ]. destruct b as [| b]; [ exfalso; apply Hb; reflexivity | simpl ]. destruct a as [a| ]; [ simpl | reflexivity ]. rewrite divmod_div. rewrite Nat.div_mul; [ reflexivity | idtac ]. intros H; discriminate H. Qed.
imports: Utf8 Compare_dec NPeano Misc