Definition natlehnplusnm (n m : nat) : n ≤ n + m. Proof. intros. induction m as [|m M]. - induction (!natplusr0 n). apply isreflnatleh. - induction (plus_n_Sm n m). apply natlehtolehs. assumption. Defined.