Lemma nattruncautoinvisnattruncauto { upper : nat } { i : nat -> nat } ( p : isnattruncauto upper i ) : isnattruncauto upper ( nattruncautoinv p ). Proof. intros. split. - intros n n'. split with ( i n ). split. + apply (pr2 p). assumption. + split. * unfold nattruncautoinv. destruct ( natgthorleh ( i n ) upper ) as [ l | r ]. -- apply fromempty. apply ( isirreflnatlth ( i n ) ). apply ( natlehlthtrans _ upper ). ++ apply (pr2 p). assumption. ++ assumption. -- apply ( nattruncautoisinj p ). ++ apply ( nattruncautopreimageineq ). ++ assumption. ++ apply ( nattruncautopreimagepath p r ). * intros m x v. unfold nattruncautoinv in v. destruct ( natgthorleh m upper ) as [ l | r ]. -- apply fromempty. apply ( isirreflnatlth upper ). apply ( natlthlehtrans _ m ); assumption. -- rewrite <- v. apply ( nattruncautopreimagepath p r ). - intros x X. unfold nattruncautoinv. destruct ( natgthorleh x upper ) as [ l | r ]. * assumption. * apply ( nattruncautopreimageineq p r ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.