Definition truncnattruncauto { upper : nat } { i : nat -> nat } ( p : isnattruncauto ( S upper ) i ) : nat -> nat. Proof. intros n. destruct ( natlthorgeh ( i n ) ( S upper ) ) as [ l | r ]. - exact ( i n ). - destruct ( natgehchoice _ _ r ) as [ a | b ]. + exact ( i n ). + destruct ( isdeceqnat n ( S upper ) ) as [ h | k ]. * exact ( i n ). * exact ( i ( S upper ) ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.