Lemma doubleminuslehpaths ( n m : nat ) ( p : natleh m n ) : sub n (sub n m ) = m. Proof. revert m p. induction n. - intros m p. destruct ( natlehchoice m 0 p ) as [ h | k ]. + apply fromempty. apply negnatlthn0 with ( n := m ). assumption. + simpl. apply pathsinv0. assumption. - intros. destruct m. + simpl. apply minusnn0. + change ( sub ( S n ) (sub n m ) = S m ). rewrite <- pathssminus. * rewrite IHn. -- apply idpath. -- assumption. * apply ( minuslth ( S n ) ( S m ) ). -- apply (natlehlthtrans _ n ). ++ apply natleh0n. ++ apply natlthnsn. -- apply (natlehlthtrans _ m ). ++ apply natleh0n. ++ apply natlthnsn. 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.