Definition natlthandminusl (n m k : nat) (is : natgth n m) (is' : natgeh k n) : natlth (k - n) (k - m). Proof. intro n. induction n as [ | n IHn ]. intros. destruct (negnatgth0n _ is). intro m. induction m. intros. destruct k. destruct (negnatgeh0sn _ is'). apply (natlehlthtrans _ k _). apply (natminuslehn k n). apply natlthnsn. intro k. induction k. intros is is'. destruct (negnatgeh0sn _ is'). intros is is'. apply (IHn m k is is'). Defined.