Definition natgthandminusinvr (n m k : nat) (is : natgth n m) (is' : natgth n k) : natgth (n - k) (m - k). Proof. intro n. induction n as [ | n IHn ]. intros. destruct (negnatgth0n _ is). intro m. induction m. intros. destruct k. apply natgthsn0. apply (IHapply natgehn0. intro k. induction k. intro is. apply is. intro is. apply (IHn m k is). Defined.