Lemma nattruncreverseisnattruncauto ( upper : nat ) : isnattruncauto upper ( nattruncreverse upper ). Proof. intros. unfold isnattruncauto. split. - intros m q. set ( m' := sub upper m ). assert ( natleh m' upper ) as a0 by apply minusleh. assert ( nattruncreverse upper m' = m ) as a1. { unfold nattruncreverse. + destruct ( natgthorleh m' upper ). * apply fromempty. apply isirreflnatlth with ( n := m' ). apply natlehlthtrans with ( m := upper ). -- assumption. -- assumption. * unfold m'. rewrite doubleminuslehpaths. -- apply idpath. -- assumption. } split with m'. split. + assumption. + split. * assumption. * intros n qq u. unfold m'. rewrite <- u. unfold nattruncreverse. destruct ( natgthorleh n upper ) as [ l | r ]. -- apply fromempty. apply ( isirreflnatlth n ). apply ( natlehlthtrans _ upper ). ++ assumption. ++ assumption. -- rewrite doubleminuslehpaths. ++ apply idpath. ++ assumption. - intros x X. unfold nattruncreverse. destruct ( natgthorleh x upper ) as [ l | r ]. + assumption. + apply minusleh. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.