proposition: Lemma cardinals_ltP a: cardinalp a -> (forall b, inc b (cardinals_lt a) <-> (b <c a)).
proof: Proof. move=> cx y; split; first by move /Zo_P => [bs cb]. by move => h; move: (oclt h) => /(oltP0) [ _ _ yx]; apply /Zo_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)