fact: Definition nattruncautopreimageineq { upper : nat } { i : nat -> nat } ( p : isnattruncauto upper i ) { n : nat } ( n' : natleh n upper ) : natleh ( nattruncautopreimage p n' ) upper := pr1 ( pr2 ( pr1 p n n' ) ).
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.NumberSystems.Integers