Lemma minus1leh { n m : nat } ( p : natlth 0 n ) ( q : natlth 0 m ) ( r : natleh n m ) : natleh ( sub n 1 ) ( sub m 1 ). Proof. revert m p q r. destruct n. - auto. - intros m p q r. destruct m. + apply fromempty. exact (isirreflnatlth 0%nat q ). + assert ( natleh n m ) as a. { apply r. } assert ( natleh ( sub n 0%nat ) m ) as a0. { exact (transportf ( fun x : nat => natleh x m ) ( pathsinv0 ( minus0r n ) ) a). } exact ( transportf ( fun x : nat => natleh ( sub n 0 ) x ) (pathsinv0 ( minus0r m ) ) a0 ). 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.