Definition nattruncautoinv { upper : nat } { i : nat -> nat } ( p : isnattruncauto upper i ) : nat -> nat. Proof. intros n. destruct ( natgthorleh n upper ) as [ l | r ]. - exact n. - exact ( nattruncautopreimage p r ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.