Lemma truncnattruncautoisinj { upper : nat } { i : nat -> nat } ( p : isnattruncauto ( S upper ) i ) { n m : nat } ( q : natleh n upper ) ( r : natleh m upper ) : truncnattruncauto p n = truncnattruncauto p m -> n = m. Proof. intros s. apply ( nattruncautoisinj p ). - apply natlthtoleh. apply ( natlehlthtrans _ upper ). + assumption. + apply natlthnsn. - apply natlthtoleh. apply ( natlehlthtrans _ upper ). + assumption. + apply natlthnsn. - unfold truncnattruncauto in s. destruct ( natlthorgeh ( i n ) ( S upper ) ) as [ a0 | a1 ]. + destruct ( natlthorgeh ( i m ) ( S upper ) ) as [ b0 | b1 ]. * assumption. * apply fromempty. assert ( i m = S upper ) as f0. { destruct ( natgehchoice ( i m ) ( S upper ) b1 ) as [ l | l' ]. -- apply fromempty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ ( i n ) ). ++ rewrite s. assumption. ++ assumption. -- assumption. } destruct (natgehchoice ( i m ) ( S upper ) b1 ) as [ a00 | a10 ]. -- apply (isirreflnatgth ( S upper ) ). rewrite f0 in a00. assumption. -- destruct ( isdeceqnat m ( S upper ) ) as [ a000 | a100 ]. ++ rewrite s in a0. rewrite f0 in a0. apply ( isirreflnatlth ( S upper ) ). assumption. ++ assert ( i m = n ) as f1. { apply ( nattruncautoisinj p ). ** rewrite f0. apply isreflnatleh. ** apply natlthtoleh. apply ( natlehlthtrans _ upper ). --- assumption. --- apply natlthnsn. ** rewrite f0. rewrite s. apply idpath. } apply ( isirreflnatlth upper ). apply ( natlthlehtrans _ n ). ** rewrite <- f1, f0. apply natlthnsn. ** assumption. + destruct ( natgehchoice ( i n ) ( S upper ) a1 ) as [ a00 | a01 ]. * apply fromempty. apply ( isirreflnatlth ( S upper ) ). apply ( natlthlehtrans _ ( i n ) ). -- assumption. -- apply ( pr2 p ). apply natlthtoleh. apply ( natlehlthtrans _ upper ). ++ assumption. ++ apply natlthnsn. * destruct ( natlthorgeh ( i m ) ( S upper ) ) as [ b0 | b1 ]. -- destruct ( isdeceqnat n ( S upper ) ) as [ a000 | a001 ]. ++ assumption. ++ assert ( S upper = m ) as f0. { apply ( nattruncautoisinj p ). ** apply isreflnatleh. ** apply natlthtoleh. apply ( natlehlthtrans _ upper ). --- assumption. --- apply natlthnsn. ** assumption. } apply fromempty. apply a001. rewrite f0. apply fromempty. apply ( isirreflnatlth ( S upper ) ). apply ( natlehlthtrans _ upper ). ** rewrite f0. assumption. ** apply natlthnsn. -- destruct ( natgehchoice ( i m ) ( S upper ) b1 ) as [ b00 | b01 ]. ++ apply fromempty. apply ( isirreflnatlth ( i m ) ). apply ( natlehlthtrans _ ( S upper ) ). ** apply (pr2 p). apply ( natlthtoleh ). apply ( natlehlthtrans _ upper ). --- assumption. --- apply natlthnsn. ** assumption. ++ rewrite b01. rewrite a01. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.