proposition: Theorem div_lt_upper_bound : ∀ a b q, b ≠ 0 → b ≠ ∞ → a < b * q → a / b < q.
proof: Proof. intros a b q Hb Hbi Ha. destruct a as [a| ]. destruct b as [b| ]. destruct q as [q| ]; [ idtac | constructor ]. apply fin_lt_mono. destruct b as [| b]. exfalso; revert Ha; apply nlt_0_r. apply Nat.div_lt_upper_bound. intros H; discriminate H. apply fin_lt_mono; assumption. exfalso; apply Hbi; reflexivity. destruct b as [b| ]; [ inversion Ha | idtac ]. exfalso; apply Hbi; reflexivity. Qed.
imports: Utf8 Compare_dec NPeano Misc