Lemma natleplusminus k m n : k + m ≤ n -> k ≤ n - m. Proof. intros i. apply (natlehandplusrinv _ _ m). rewrite minusplusnmm. { exact i. } { change (m ≤ n). simple refine (istransnatleh _ i); clear i. apply natlehmplusnm. } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.