Lemma natlehtole (n m : nat) : n ≤ m -> le n m. Proof. intros H. induction m as [|m IHm]. - assert (int := natleh0tois0 H). clear H. destruct int. apply le_n. - set (int2 := natlehchoice2 n (S m) H). destruct int2 as [ isnatleh | iseq ]. apply (le_S n m (IHm isnatleh)). destruct iseq. apply le_n. Defined.