proposition: Lemma natlthsntoleh ( n m : nat ) : natlth m ( S n ) -> natleh m n.
proof: Proof. revert m. induction n. - intros m p. destruct m. + apply isreflnatleh. + assert ( natlth m 0 ) as q by apply p. apply fromempty. exact ( negnatgth0n m q ). - intros m p. destruct m. + apply natleh0n. + apply ( IHn m ). 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