Lemma nattruncautocompstable { R : commring } { upper : nat } ( i j : nat -> nat ) ( p : isnattruncauto upper i ) ( p' : isnattruncauto upper j ) : isnattruncauto upper ( funcomp j i ). Proof. intros. split. - intros n n'. split with ( nattruncautopreimage p' ( nattruncautopreimageineq p n' ) ). split. + apply ( nattruncautopreimageineq p' ). + split. * simpl. rewrite ( nattruncautopreimagepath p' _ ). rewrite ( nattruncautopreimagepath p _ ). apply idpath. * intros x X y. simpl in y. apply ( nattruncautoisinj p' ). -- apply nattruncautopreimageineq. -- assumption. -- apply ( nattruncautoisinj p ). ++ apply (pr2 p'). apply nattruncautopreimageineq. ++ apply (pr2 p') . assumption. ++ rewrite ( nattruncautopreimagepath p' ). rewrite ( nattruncautopreimagepath p ). rewrite y. apply idpath. - intros x X. apply (pr2 p). apply (pr2 p'). assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.