Definition natminuslehn (n m : nat) : n - m <= n. Proof. revert m. induction n as [ | n IHn ]. - intro. apply isreflnatleh. - intro. destruct m as [ | m ]. + apply isreflnatleh. + simpl. apply (istransnatleh (IHn m) (natlehnsn n)). Defined.