Lemma natlthsnminussmsn ( n m : nat ) ( p : natlth m n ) : natlth ( sub ( S n ) ( S m ) ) ( S n ). Proof. revert m p. induction n. - intros m p. apply fromempty. apply (negnatlthn0 m p). - intros m p. destruct m. + assert ( sub ( S ( S n ) ) 1 = S n ) as f. { destruct n. * auto. * auto. } rewrite f. apply natlthnsn. + apply ( istransnatlth _ ( S n ) _ ). * apply IHn. assumption. * apply natlthnsn. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Algebra.Monoids.