Definition natminuseqlr m n x : m≤n -> n-m = x -> n = x+m. Proof. intros i j. rewrite <- (minusplusnmm _ _ i). rewrite j. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.