proposition: Lemma natlthminus0 { n m : nat } ( p : natlth m n ) : natlth 0 ( sub n m ).
proof: Proof. revert m p. induction n. - intros m p. apply fromempty. exact ( negnatlthn0 m p ). - intros m p. destruct m. + auto. + apply IHn. apply p. 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