proposition: Theorem add_lt_mono_l : ∀ n m p, p ≠ ∞ → n < m ↔ p + n < p + m.
proof: Proof. intros n m p Hp. rewrite add_comm. replace (p + m) with (m + p) by apply add_comm. apply add_lt_mono_r; assumption. Qed.
imports: Utf8 Compare_dec NPeano Misc