proposition: Lemma sincr_bounded_unique h y y' a: sincr_ofs h -> ordinalp y -> ordinalp y' -> (h y) <=o a -> a <o h (osucc y) -> (h y') <=o a -> a <o (h (osucc y')) -> y = y'.
proof: Proof. move=> oih oy oy' le1 le2 le3 le4. wlog: y y' oy oy' le1 le2 le3 le4 / y <o y'. case: (oleT_ell oy oy') => // ll; first by apply. by move=> aux;symmetry; apply: aux. have lt2:=(ole_ltT le3 le2). move /oleSltP => h2. case: (equal_or_not (osucc y) y'). by move=> h3; move: lt2=> [_]; rewrite h3. move=> h3; have h4: (osucc y) <o y' by split. move: (oih _ _ h4) => [/(oltNge lt2) []]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)