proposition: Lemma plusmn0n0 m n : m + n = 0 -> n = 0.
proof: Proof. intros i. assert (a := natlehmplusnm m n). rewrite i in a. apply natleh0tois0. assumption. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA