proposition: Lemma eq_subset_cardP1 x y:x <=s y <-> x <=cc y.
proof: Proof. apply: (iff_trans (eq_subset_cardP x y)). split; first by move/cardinal_le_aux2P; apply; fprops. apply: cardinal_le_aux1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)