Definition nattruncreverse ( upper : nat ) : nat -> nat. Proof. intros n. destruct ( natgthorleh n upper ) as [ h | k ]. - exact n. - exact ( sub upper n ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.