Lemma nattruncbottomtopswapbound ( upper n : nat ) ( p : natleh n upper ) : natleh (nattruncbottomtopswap upper n ) upper. Proof. intros. unfold nattruncbottomtopswap. destruct (isdeceqnat 0%nat n). - auto. destruct ( isdeceqnat upper n ). + apply isreflnatleh. + apply isreflnatleh. - destruct ( isdeceqnat upper n ). + apply natleh0n. + assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.