proposition: Lemma nattruncbottomtopswapbound ( upper n : nat ) ( p : natleh n upper ) : natleh (nattruncbottomtopswap upper n ) upper.
proof: 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.
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.NumberSystems.Integers