Definition natgehandminusl (n m k : nat) (is : n ≥ m) : n - k ≥ m - k. Proof. revert m k is. induction n as [ | n IHn ]. - intros. rewrite (nat0gehtois0 _ is). apply isreflnatleh. - intro m. induction m. + intros. destruct k. * apply natgehn0. * apply natgehn0. + intro k. induction k. * intro is. apply is. * intro is. apply (IHn m k is). Defined.