Definition natassocpmineq (n m k : nat) : natleh ((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 (natplusr0 n). destruct (boolchoice (natgtb k (n+m))) as [ g' | le']. set (e' := minuseq0 (n+m) k (natgthtogeh _ _ g')). rewrite e'. apply natleh0n. apply (natlehandplusrinv _ _ k). rewrite (minusplusnmm _ k). apply natlehandplusl. apply (natlthtoleh _ _ g). set (int := falsetonegtrue _ le'). assumption. rewrite (natassocpmeq _ _ _ le). apply isreflnatleh. Defined.