Definition nattruncbottomtopswap ( upper : nat ) : nat -> nat. Proof. intros n. destruct ( isdeceqnat 0%nat n ) as [ h | k ]. - exact upper. - destruct ( isdeceqnat upper n ) as [ l | r ]. + exact ( 0%nat ). + exact n. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.