Lemma natltminus1 m n : m < n -> m ≤ n - 1. Proof. intros i. assert (a := natlthp1toleh m (n - 1)). assert (b := natleh0n m). assert (c := natlehlthtrans _ _ _ b i). assert (d := natlthtolehsn _ _ c). assert (e := minusplusnmm _ _ d). rewrite e in a. exact (a i). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.