proposition: Lemma natlehdecomp ( b a : nat ) : ( ∃ c : nat, ( a + c )%nat = b ) -> natleh a b.
proof: 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.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.NumberSystems.Integers UniMath.Algebra.Monoids