proposition: Lemma cardinals_leP a : cardinalp a -> forall b, (inc b (cardinals_le a) <-> (b <=c a)).
proof: Proof. move=> ca b; rewrite/cardinals_le; split. move /Zo_P => [/(oleP (proj1 ca)) bs cb];exact:(ocle3 cb ca bs). move => lba;apply: Zo_i; first by apply /(oleP (proj1 ca))/(ocle lba). exact: (proj31 lba). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)