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