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