Lemma nattruncautoisinj { upper : nat } { i : nat -> nat } ( p : isnattruncauto upper i ) { n m : nat } ( n' : natleh n upper ) ( m' : natleh m upper ) : i n = i m -> n = m. Proof. intros h. assert ( natleh ( i m ) upper ) as q. { apply (pr2 p). assumption. } set ( x := pr1 p ( i m ) q ). set ( v := pr1 x ). set ( w := pr1 ( pr2 x ) ). set ( y := pr1 ( pr2 ( pr2 x ) ) ). change ( pr1 x ) with v in w, y. assert ( v = n ) as a. { apply (pr2 (pr2 (pr2 x))). - assumption. - assumption. } rewrite <- a. apply (pr2 (pr2 ( pr2 x))). - assumption. - apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.