Lemma nattruncbottomtopswapselfinv ( upper n : nat ) : nattruncbottomtopswap upper ( nattruncbottomtopswap upper n ) = n. Proof. intros. unfold nattruncbottomtopswap. destruct ( isdeceqnat upper n ) as [ i | e ]. - destruct ( isdeceqnat 0%nat n ) as [i0 | _ ]. + destruct ( isdeceqnat 0%nat upper ) as [ i1 | e1 ]. * rewrite <- i0. rewrite <- i1. apply idpath. * apply fromempty. apply e1. rewrite i. rewrite i0. apply idpath. + destruct ( isdeceqnat 0%nat 0%nat ) as [ _ | e1 ]. * assumption. * apply fromempty. apply e1. auto. - destruct ( isdeceqnat 0%nat n ) as [i0 | e0 ]. + destruct ( isdeceqnat 0%nat upper ) as [ i1 | _ ]. * rewrite <- i0. rewrite i1. apply idpath. * destruct ( isdeceqnat upper upper ) as [ _ | e2 ]. -- assumption. -- apply fromempty. apply e2. auto. + destruct ( isdeceqnat 0%nat n ) as [ i1 | _ ]. * apply fromempty. apply e0. assumption. * destruct ( isdeceqnat upper n ) as [ i2 | _ ]. -- apply fromempty. apply e. assumption. -- apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.