Lemma natplusminus m n k : k=m+n -> k-n=m. Proof. intros i. rewrite i. apply plusminusnmm. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.