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