proposition: Theorem lt_sub_lt_add_l : ∀ n m p, n ≠ ∞ → n - m < p → n < m + p.
proof: Proof. intros n m p Hn H. destruct m as [m| ]. destruct p as [p| ]. destruct n as [n| ]; [ simpl in H; simpl | inversion H ]. apply lt_qfin. apply qfin_lt_mono in H. apply Qlt_sub_lt_add_l; assumption. destruct n as [n| ]; [ constructor | inversion H ]. destruct n as [n| ]; [ constructor | idtac ]. exfalso; apply Hn; reflexivity. Qed.
imports: Utf8 QArith Misc