proposition: Lemma minusnleh1 ( n m : nat ) ( p : natlth m n ) : natleh m ( sub n 1 ).
proof: Proof. revert m p. destruct n. - intros m p. apply fromempty. exact (negnatlthn0 m p ). - intros m p. destruct m. + apply natleh0n. + apply natlthsntoleh. change ( sub ( S n ) 1 ) with ( sub n 0 ). rewrite minus0r. assumption. Defined.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.NumberSystems.Integers UniMath.Algebra.Monoids