Lemma natlehdecomp ( b a : nat ) : ( ∃ c : nat, ( a + c )%nat = b ) -> natleh a b. Proof. revert a. induction b. - intros a p. use (hinhuniv _ p). intro t. destruct t as [ c f ]. destruct a. + apply isreflnatleh. + apply fromempty. simpl in f . exact ( negpathssx0 ( a + c ) f ). - intros a p. use (hinhuniv _ p). intro t. destruct t as [ c f ]. destruct a. + apply natleh0n. + assert ( natleh a b ) as q. { simpl in f. apply IHb. intro P. intro s. apply s. split with c. apply invmaponpathsS. assumption. } apply q. 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.