Lemma nattruncbottomtopswapisnattruncauto ( upper : nat ) : isnattruncauto upper ( nattruncbottomtopswap upper ). Proof. intros. unfold isnattruncauto. split. - intros m p. set ( m' := nattruncbottomtopswap upper m ). assert ( natleh m' upper ) as a0. { apply nattruncbottomtopswapbound. assumption. } assert (nattruncbottomtopswap upper m' = m) as a1 by apply nattruncbottomtopswapselfinv. split with m'. split. + assumption. + split. * assumption. * intros k q u. unfold m'. rewrite <- u. rewrite nattruncbottomtopswapselfinv. apply idpath. - intros n p. apply nattruncbottomtopswapbound. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.