proposition: Lemma ordinal_inA x y: ordinalp x -> ordinalp y -> [\/ inc x y, inc y x | x = y].
proof: Proof. move=> ox oy. have aux: (ordinal_set (doubleton x y)) by move=> a /set2_P [] ->. case /set2_P: (ordinal_setI (set2_ne x y) aux). move/setI2id_Pl => h;case: (ordinal_sub ox oy h) => p; in_TP4. move/setI2id_Pr => h;case: (ordinal_sub oy ox h); in_TP4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)