Lemma natplusminusle {a b c} : b ≥ c -> a+(b-c) = (a+b)-c. Proof. intros e. assert (E := minusplusnmm b c e). rewrite <- E. clear E e. rewrite <- natplusassoc. rewrite plusminusnmm. rewrite plusminusnmm. apply idpath. Defined.