Lemma natminusminus n m : m ≤ n -> n - (n - m) = m. Proof. intros i. assert (b := plusminusnmm m (n-m)). rewrite natpluscomm in b. rewrite (minusplusnmm _ _ i) in b. exact b. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.