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