Lemma natminus0le {m n} : m-n = 0 -> n ≥ m. Proof. intros i. apply negnatgthtoleh. intro k. assert (r := minusgth0 _ _ k); clear k. induction (!i); clear i. exact (negnatgth0n 0 r). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.