Definition isnattruncauto ( upper : nat ) ( i : nat -> nat ) := ( forall x : nat, natleh x upper -> ∑ (y : nat), natleh y upper × ( i y = x × forall z : nat, natleh z upper -> i z = x -> y = z ) ) × forall x : nat, natleh x upper -> natleh ( i x ) upper.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.