Lemma precompwithnatcofaceisauto { upper : nat } ( i : nat -> nat ) ( p : isnattruncauto ( S upper ) i ) ( bound : natlth 0 ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ) ) : isnattruncauto upper (funcomp ( natcoface ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ) ) i ). Proof. intros. set ( v := nattruncautopreimage p ( isreflnatleh ( S upper ) ) ). change ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ) with v in bound. unfold isnattruncauto. split. - intros m q. unfold funcomp. assert ( natleh m ( S upper ) ) as aaa. { apply natlthtoleh. apply natlehlthtrans with ( m := upper). + assumption. + exact ( natlthnsn upper ). } set ( m' := nattruncautopreimage p aaa ). destruct ( natlthorgeh m' v ) as [ l | r ]. + split with m'. split. * apply natlthsntoleh. apply ( natlthlehtrans _ v ). -- assumption. -- apply ( nattruncautopreimageineq p _ ). * split. -- unfold natcoface. rewrite l. apply ( nattruncautopreimagepath p aaa ). -- intros n j w. assert ( natcoface v n = m' ) as f0. { apply pathsinv0. apply ( nattruncautopreimagecanon p aaa ). ++ apply natcofaceleh. assumption. ++ assumption. } rewrite <- f0. destruct ( natgthorleh v n ) as [ l' | r' ]. ++ unfold natcoface. rewrite l'. apply idpath. ++ apply fromempty. apply ( isirreflnatlth v ). apply ( natlehlthtrans _ n ). ** assumption. ** apply ( istransnatlth _ ( S n ) ). { apply natlthnsn. } unfold natcoface in f0. rewrite ( natgehimplnatgtbfalse v n r' ) in f0. rewrite f0. assumption. + set ( j := nattruncautopreimagepath p aaa ). change ( nattruncautopreimage p aaa ) with m' in j. set ( m'' := sub m' 1 ). assert ( natleh m'' upper ) as a0. { destruct ( natlthorgeh 0 m' ) as [ h | h' ]. * rewrite <- ( minussn1 upper ). apply minus1leh. -- assumption. -- apply ( natlehlthtrans _ upper ). ++ apply natleh0n. ++ apply natlthnsn. -- apply nattruncautopreimageineq. * destruct ( natgehchoice 0 m' h' ) as [ k | k' ]. -- apply fromempty. apply ( negnatgth0n m' k ). -- unfold m''. rewrite <- k'. apply natleh0n. } destruct ( natgehchoice m' v r ) as [ l' | r' ]. * assert ( natleh v m'' ) as a2. { apply natlthsntoleh. unfold m''. rewrite pathssminus. -- rewrite minussn1. assumption. -- destruct ( natlehchoice 0 m' ( natleh0n m' ) ) as [ k | k' ]. ++ assumption. ++ apply fromempty. apply ( negnatgth0n v ). rewrite k'. assumption. } assert ( i ( natcoface v m'' ) = m ) as a1. { unfold natcoface. rewrite ( natgehimplnatgtbfalse v m'' a2 ). unfold m''. rewrite pathssminus. -- rewrite minussn1. assumption. -- destruct ( natlehchoice 0 m' ( natleh0n m' ) ) as [ k | k' ]. ++ assumption. ++ apply fromempty. apply ( negnatgth0n v ). rewrite k'. assumption. } split with m''. split. -- assumption. -- split. ++ assumption. ++ intros n s t. assert ( natcoface v n = natcoface v m'' ) as g. { assert ( natcoface v n = m' ) as g0. { apply pathsinv0. apply ( nattruncautopreimagecanon p aaa ). ** apply natcofaceleh. assumption. ** assumption. } assert ( natcoface v m'' = m' ) as g1. { unfold m'. unfold nattruncautopreimage. apply pathsinv0. apply ( nattruncautopreimagecanon p aaa ). ** apply natcofaceleh. assumption. ** assumption. } rewrite g0, g1. apply idpath. } change ( idfun _ m'' = idfun _ n ). rewrite <- ( natcofaceretractisretract v ). simpl. rewrite g. apply idpath. * apply fromempty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). -- assert ( S upper = m ) as g. { rewrite <- ( nattruncautopreimagepath p ( isreflnatleh ( S upper ) ) ). change ( i v = m ). rewrite <- j. rewrite r'. apply idpath. } rewrite g. assumption. -- apply natlthnsn. - intros x X. assert ( natleh ( i ( natcoface v x ) ) ( S upper ) ) as a0. { apply (pr2 p). apply natcofaceleh. assumption. } destruct ( natlehchoice _ _ a0 ) as [ l | r ]. + apply natlthsntoleh. assumption. + assert ( v = natcoface v x ) as g. { unfold v. apply ( nattruncautopreimagecanon p ( isreflnatleh ( S upper ) ) ). * unfold natcoface. -- destruct ( natgthorleh v x ) as [ a | b ]. ++ unfold v in a. rewrite a. apply natlthtoleh. apply ( natlehlthtrans _ upper ). ** assumption. ** apply natlthnsn. ++ unfold v in b. rewrite ( natgehimplnatgtbfalse _ x b ). assumption. * assumption. } apply fromempty. destruct ( natgthorleh v x ) as [ a | b ]. * unfold natcoface in g. rewrite a in g. apply ( isirreflnatlth x ). rewrite g in a. assumption. * unfold natcoface in g. rewrite ( natgehimplnatgtbfalse v x b ) in g. apply ( isirreflnatlth x ). apply ( natlthlehtrans _ ( S x ) ). -- apply natlthnsn. -- rewrite <- g. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.