proposition: Lemma natlehsnminussmsn ( n m : nat ) ( p : natleh m n ) : natleh (sub ( S n ) ( S m ) ) ( S n ).
proof: Proof. revert m p. induction n. - intros m p. apply negnatgthtoleh. intro X. apply nopathsfalsetotrue. assumption. - intros m p. destruct m. + apply natlthtoleh. apply natlthnsn. + apply ( istransnatleh( m := S n ) ). * apply IHn. assumption. * apply natlthtoleh. apply natlthnsn. 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