proposition: Theorem lt_sub_lt_add_r : ∀ n m p, n ≠ ∞ → n - p < m → n < m + p.
proof: Proof. intros n m p Hn H. destruct n as [n| ]. destruct m as [m| ]; [ simpl | constructor ]. destruct p as [p| ]; [ idtac | constructor ]. constructor; apply Nat.lt_sub_lt_add_r. inversion H; subst; assumption. negation Hn. Qed.
imports: Utf8 Compare_dec NPeano Misc