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