Definition natassocmpineq (n m k : nat) : natgeh ((n - m) + k) (n - (m - k)). Proof. intros k. destruct (natgthorleh k m) as [g | le]. set (e := minuseq0 m k (natgthtogeh _ _ g)). rewrite e. rewrite (natminuseqn n). apply (natgehandplusrinv _ _ m). rewrite (natplusassoc _ _ m). rewrite (natpluscomm _ m). destruct (natplusassoc (n - m) m k). assert (int1 : natgeh (n - m + m + k) (n + k)). apply (natgehandplusr _ _ k). apply minusplusnmmineq. assert (int2 : natgeh (n + k) (n + m)). apply (natgehandplusl _ _ n). apply (natgthtogeh _ _ g). apply (istransnatgeh _ _ _ int1 int2). destruct (natgthorleh m n) as [g' | le']. rewrite (minuseq0 _ _ (natgthtogeh _ _ g')). change (0 + k) with k. apply (natgehandplusrinv _ _ (m - k)). rewrite (natpluscomm k _). rewrite (minusplusnmm _ _ le). destruct (natgthorleh (m - k) n) as [ g'' | le'' ]. rewrite (minuseq0 n (m - k) (natgthtogeh _ _ g'')). apply (natminuslehn m k). rewrite (minusplusnmm _ _ le''). apply (natgthtogeh _ _ g'). rewrite (natassocmpeq _ _ _ le' le). apply isreflnatgeh. Defined.