Definition natgehandminuslinv (n m k : nat) (is' : natgeh k n) (is : natleh (k - n) (k - m)) : natgeh n m. Proof. intros. set (int := natgehgthtrans _ (k - n) _ is (minusgeh0 _ _ is')). set (int' := minusgeh0inv _ _ int). set (int'' := natlehandplusr _ _ n is). rewrite (minusplusnmm _ _ (natgthtogeh _ _ is')) in int''. set (int''' := natlehandplusr _ _ m int''). rewrite (natplusassoc _ n _) in int'''. rewrite (natpluscomm n m) in int'''. destruct (natplusassoc (k - m) m n) in int'''. rewrite (minusplusnmm _ _ (natgthtogeh _ _ int')) in int'''. apply (natgehandpluslinv _ _ k). apply int'''. Defined.