proposition: Lemma cardinal_le_aux2P x y: cardinalp x -> cardinalp y -> (x <=s y <-> x <=c y).
proof: Proof. move=> cx cy. split; last by apply: cardinal_le_aux1. move => /set_leP [z zy ezx]; split => //. case:(oleT_ee (OS_cardinal cx)(OS_cardinal cy)) => [] [_ _ ] => // syx. suff: y \Eq x. by move/card_eqP; rewrite (card_card cx) (card_card cy) => ->. apply:(CantorBernstein (set_le_t syx)). by apply/set_leP; exists z. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)