Definition natlehandminusl (n m k : nat) (is : natgeh n m) : natgeh (k - m) (k - n). Proof. intro n. induction n as [ | n IHn ]. intros. rewrite (nat0gehtois0 _ is). apply isreflnatleh. intro m. induction m. intros. destruct k. apply natminuslehn. apply natminuslehn. intro k. induction k. intro is. apply isreflnatleh. intro is. apply (IHn m k). apply is. Defined.