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