proposition: Theorem succ_lt_mono : ∀ n m, n < m ↔ NS n < NS m.
proof: Proof. intros n m. split; intros H. destruct n as [n| ]; [ simpl | destruct m; inversion H ]. destruct m as [m| ]; [ simpl | constructor ]. apply fin_lt_mono, Nat.succ_lt_mono in H. apply fin_lt_mono; assumption. destruct n as [n| ]; [ simpl | destruct m; inversion H ]. destruct m as [m| ]; [ simpl in H | constructor ]. apply fin_lt_mono, Nat.succ_lt_mono. apply fin_lt_mono; assumption. Qed.
imports: Utf8 Compare_dec NPeano Misc