proposition: Theorem le_add_r : ∀ n m, n ≤ n + m.
proof: Proof. intros n m. destruct n as [n| ]; [ idtac | constructor ]. destruct m as [m| ]; [ simpl | constructor ]. apply le_fin, Nat.le_add_r. Qed.
imports: Utf8 Compare_dec NPeano Misc