proposition: Lemma succ_inf_aux_ord x y: ordinalp x -> ordinalp y -> ((osucc x) \Eq (osucc y) <-> x \Eq y).
proof: Proof. move=> /ordinal_irreflexive xa /ordinal_irreflexive yb; split. move => fp; exact:(succ_inf_aux_p2 xa yb fp). move => fp; exact:(succ_inf_aux_p1 xa yb fp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)