Lemma truncnattruncautobound { upper : nat } ( i : nat -> nat ) ( p : isnattruncauto ( S upper ) i ) ( n : nat ) ( q : natleh n upper ) : natleh ( truncnattruncauto p n ) upper. Proof. intros. unfold truncnattruncauto. destruct ( natlthorgeh ( i n ) ( S upper) ) as [ l | r ]. - apply natlthsntoleh. assumption. - destruct ( natgehchoice ( i n ) ( S upper ) ) as [ l' | r' ]. + apply fromempty. apply ( isirreflnatlth ( i n ) ). apply ( natlehlthtrans _ ( S upper ) ). * apply (pr2 p). apply natlthtoleh. apply ( natlehlthtrans _ upper ). -- assumption. -- apply natlthnsn. * assumption. + destruct ( isdeceqnat n ( S upper ) ) as [ l'' | r'' ]. * apply fromempty. apply ( isirreflnatlth upper ). apply ( natlthlehtrans _ ( S upper ) ). -- apply natlthnsn. -- rewrite <- l''. assumption. * assert ( natleh ( i ( S upper ) ) ( S upper ) ) as aux. { apply (pr2 p). apply isreflnatleh. } destruct ( natlehchoice _ _ aux ) as [ l''' | r''' ]. -- apply natlthsntoleh. assumption. -- apply fromempty. apply r''. apply ( nattruncautoisinj p ). ++ apply natlthtoleh. apply ( natlehlthtrans _ upper ). ** assumption. ** apply natlthnsn. ++ apply isreflnatleh. ++ rewrite r'. rewrite r'''. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.