Definition nattruncautopreimagecanon { upper : nat } { i : nat -> nat } ( p : isnattruncauto upper i ) { n : nat } ( n' : natleh n upper ) { m : nat } ( m' : natleh m upper ) ( q : i m = n ) : nattruncautopreimage p n' = m := pr2 ( pr2 ( pr2 ( pr1 p n n' ) ) ) m m' q.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.