Lemma minusnleh1 ( n m : nat ) ( p : natlth m n ) : natleh m ( sub n 1 ). Proof. revert m p. destruct n. - intros m p. apply fromempty. exact (negnatlthn0 m p ). - intros m p. destruct m. + apply natleh0n. + apply natlthsntoleh. change ( sub ( S n ) 1 ) with ( sub n 0 ). rewrite minus0r. assumption. 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.