proposition: Lemma ordo_ltP x a b: ordinalp x -> inc a x -> inc b x -> (glt (ordinal_o x) a b <-> inc a b).
proof: Proof. move=> ox ax bx. have ob:= (Os_ordinal ox bx). split. move => [/ordo_leP [_ _ sab]] nab. by case: (ordinal_sub (Os_ordinal ox ax) ob sab). by move => /(ordinal_sub2 ob) [sab nab]; split => //;apply /ordo_leP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)