Definition truncnattruncautoinv { upper : nat } { i : nat -> nat } ( p : isnattruncauto ( S upper ) i ) : nat -> nat := nattruncautoinv ( truncnattruncautoisauto p ).
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.