proposition: Theorem add_lt_mono_r : ∀ n m p, p ≠ ∞ → n < m ↔ n + p < m + p.
proof: Proof. intros n m p Hp. split; intros H. destruct n as [n| ]. destruct m as [m| ]. destruct p as [p| ]. constructor; apply Nat.add_lt_mono_r; inversion H; assumption. negation Hp. destruct p as [p| ]; [ constructor | negation Hp ]. destruct m; inversion H. destruct n as [n| ]; [ idtac | inversion H ]. destruct m as [m| ]; [ idtac | constructor ]. destruct p as [p| ]; [ idtac | inversion H ]. constructor; inversion H; apply Nat.add_lt_mono_r in H2; assumption. Qed.
imports: Utf8 Compare_dec NPeano Misc