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