Definition nattruncautopreimage { upper : nat } { i : nat -> nat } ( p : isnattruncauto upper i ) { n : nat } ( n' : natleh n upper ) : nat := pr1 ( pr1 p n n' ).
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.