Lemma natlthminus0 { n m : nat } ( p : natlth m n ) : natlth 0 ( sub n m ). 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.
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.