proposition: Theorem add_lt_le_mono : ∀ n m p q, p ≠ ∞ → n < m → p ≤ q → n + p < m + q.
proof: Proof. intros n m p q Hp Hnm Hpq. destruct m as [m| ]; simpl. destruct n as [n| ]; [ idtac | inversion Hnm ]. apply qfin_lt_mono in Hnm. destruct q as [q| ]; simpl. destruct p as [p| ]; [ idtac | inversion Hpq ]. apply qfin_le_mono in Hpq. apply qfin_lt_mono. apply Qplus_lt_le_compat; assumption. destruct p as [p| ]; [ constructor | idtac ]. exfalso; apply Hp; reflexivity. destruct p as [p| ]; [ idtac | exfalso; apply Hp; reflexivity ]. destruct n as [n| ]; [ idtac | inversion Hnm ]. constructor. Qed.
imports: Utf8 QArith Misc