Lemma isnattruncauto0S { upper : nat } { i : nat -> nat } ( p : isnattruncauto (S upper) i ) ( j : i 0%nat = S upper ) : isnattruncauto upper ( funcomp S i ). Proof. intros. unfold isnattruncauto. split. - intros m q. set ( v := nattruncautopreimage p (natlthtoleh m (S upper) (natlehlthtrans m upper (S upper) q (natlthnsn upper)))). destruct ( isdeceqnat 0%nat v ) as [ i0 | i1 ]. + apply fromempty. apply ( isirreflnatlth ( i 0%nat ) ). apply ( natlehlthtrans _ upper ). * rewrite i0. unfold v. rewrite nattruncautopreimagepath. assumption. * rewrite j. apply natlthnsn. + assert ( natlth 0 v ) as aux. { destruct ( natlehchoice _ _ ( natleh0n v ) ). * assumption. * apply fromempty. apply i1. assumption. } split with ( sub v 1 ). split. * rewrite <- ( minussn1 upper ). apply ( minus1leh aux ( natlehlthtrans _ _ _ ( natleh0n upper ) ( natlthnsn upper ) ) ( nattruncautopreimageineq p ( natlthtoleh m ( S upper ) ( natlehlthtrans m upper ( S upper ) q ( natlthnsn upper ) ) ) ) ). * split. -- simpl. rewrite pathssminus. ++ rewrite minussn1. apply nattruncautopreimagepath. ++ assumption. -- intros n uu k. simpl in k. rewrite <- ( minussn1 n ). assert ( v = S n ) as f. { apply ( nattruncautopreimagecanon p _ ); assumption. } rewrite f. apply idpath. - intros x X. unfold funcomp. assert ( natleh ( i ( S x ) ) ( S upper ) ) as aux. + apply (pr2 p). assumption. + destruct ( natlehchoice _ _ aux ) as [ h | k ]. * apply natlthsntoleh. assumption. * apply fromempty. assert ( 0%nat = S x ) as ii. { apply ( nattruncautoisinj p ). -- apply natleh0n. -- assumption. -- rewrite j. rewrite k. apply idpath. } apply ( isirreflnatlth ( S x ) ). apply ( natlehlthtrans _ x ). -- rewrite <- ii. apply natleh0n. -- apply natlthnsn. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.