Lemma truncnattruncautoisauto { upper : nat } { i : nat -> nat } ( p : isnattruncauto ( S upper ) i ) : isnattruncauto upper ( truncnattruncauto p ). Proof. intros. split. - intros n q. assert ( natleh n ( S upper ) ) as q'. { apply natlthtoleh. apply ( natlehlthtrans _ upper ). + assumption. + apply natlthnsn. } destruct ( isdeceqnat ( nattruncautopreimage p q' ) ( S upper ) ) as [ i0 | i1 ]. + split with ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ). split. * assert ( natleh ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ) ( S upper ) ) as aux by apply nattruncautopreimageineq. destruct ( natlehchoice _ _ aux ) as [ l | r ]. -- apply natlthsntoleh. assumption. -- assert ( n = S upper ) as f0. { rewrite <- ( nattruncautopreimagepath p q' ). rewrite i0. rewrite <- r. rewrite ( nattruncautopreimagepath p ( isreflnatleh ( S upper) ) ). rewrite r. apply idpath. } apply fromempty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). ++ rewrite <- f0. assumption. ++ apply natlthnsn. * split. -- apply ( nattruncautoisinj p ). ++ apply natlthtoleh. apply ( natlehlthtrans _ upper ). ** apply truncnattruncautobound. destruct ( natlehchoice _ _ ( nattruncautopreimageineq p ( isreflnatleh ( S upper ) ) ) ) as [ l | r]. --- apply natlthsntoleh. assumption. --- apply fromempty. assert ( S upper = n ) as f0. { rewrite <- ( nattruncautopreimagepath p ( isreflnatleh ( S upper ) ) ). rewrite r. rewrite <- i0. rewrite ( nattruncautopreimagepath p q' ). apply idpath. } apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). +++ rewrite f0. assumption. +++ apply natlthnsn. ** apply natlthnsn. ++ assumption. ++ unfold truncnattruncauto. destruct ( isdeceqnat ( nattruncautopreimage p (isreflnatleh ( S upper ) ) ) ) as [ l | r ]. ** apply fromempty. assert ( S upper = n ) as f0. { rewrite <- ( nattruncautopreimagepath p (isreflnatleh ( S upper ) ) ). rewrite l. rewrite <- i0. rewrite ( nattruncautopreimagepath p q' ). apply idpath. } apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). --- rewrite f0. assumption. --- apply natlthnsn. ** destruct ( natlthorgeh ( i ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ) ) ( S upper ) ) as [ l' | r' ]. --- apply fromempty. apply ( isirreflnatlth ( S upper ) ). rewrite ( nattruncautopreimagepath p ) in l'. assumption. --- destruct ( natgehchoice _ _ r' ) as [ l'' | r'' ]. +++ apply fromempty. apply ( isirreflnatlth ( S upper ) ). rewrite ( nattruncautopreimagepath p ) in l''. assumption. +++ rewrite <- i0. rewrite ( nattruncautopreimagepath p q' ). apply idpath. -- intros x X y. apply ( nattruncautoisinj p ). ++ apply nattruncautopreimageineq. ++ apply natlthtoleh. apply ( natlehlthtrans _ upper ). ** assumption. ** apply natlthnsn. ++ unfold truncnattruncauto in y. destruct ( natlthorgeh ( i x ) ( S upper ) ) as [ l | r ]. ** assert ( S upper = x ) as f0. { apply ( nattruncautoisinj p ). --- apply isreflnatleh. --- apply natlthtoleh. apply ( natlehlthtrans _ upper ). +++ assumption. +++ apply natlthnsn. --- rewrite <- i0. rewrite y. rewrite ( nattruncautopreimagepath p q' ). apply idpath. } apply fromempty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). --- rewrite f0. assumption. --- apply natlthnsn. ** destruct ( isdeceqnat x ( S upper ) ) as [ l' | r' ]. --- apply fromempty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). +++ rewrite <- l'. assumption. +++ apply natlthnsn. --- destruct ( natgehchoice _ _ r ) as [ l'' | r'' ]. +++ apply fromempty. apply ( isirreflnatlth n ). apply ( natlehlthtrans _ ( S upper ) ). *** assumption. *** rewrite <- y. assumption. +++ rewrite ( nattruncautopreimagepath p _ ). rewrite r''. apply idpath. + split with ( nattruncautopreimage p q' ). split. * destruct ( natlehchoice _ _ ( nattruncautopreimageineq p q' ) ) as [ l | r ]. -- apply natlthsntoleh. assumption. -- apply fromempty. apply i1. assumption. * split. -- unfold truncnattruncauto. destruct ( natlthorgeh ( i ( nattruncautopreimage p q' ) ) ( S upper ) ) as [ l | r ]. ++ apply nattruncautopreimagepath. ++ destruct ( natgehchoice _ _ r ) as [ l' | r' ]. ** apply nattruncautopreimagepath. ** apply fromempty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). --- rewrite <- r'. rewrite ( nattruncautopreimagepath p q' ). assumption. --- apply natlthnsn. -- intros x X y. apply ( nattruncautoisinj p ). ++ set (H:=pr1 p). simpl in H. set (H1:=pr2 p). simpl in H1. set (H2:=H n q'). apply (pr2 H2). ++ apply natlthtoleh. apply ( natlehlthtrans _ upper ). ** assumption. ** apply natlthnsn. ++ rewrite ( nattruncautopreimagepath p q' ). unfold truncnattruncauto in y. destruct ( natlthorgeh ( i x ) ( S upper ) ) as [ l | r ]. ** rewrite y. apply idpath. ** destruct ( isdeceqnat x ( S upper ) ) as [ l' | r' ]. --- apply fromempty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). +++ rewrite <- l'. assumption. +++ apply natlthnsn. --- destruct ( natgehchoice _ _ r ). +++ rewrite y. apply idpath. +++ apply fromempty. apply i1. apply ( nattruncautoisinj p ). *** apply ( nattruncautopreimageineq p ). *** apply isreflnatleh. *** rewrite ( nattruncautopreimagepath p q' ). rewrite y. apply idpath. - apply truncnattruncautobound. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.