proposition: Lemma eq_subset_cardP x y: x <=s y <-> (cardinal x) <=s (cardinal y).
proof: Proof. move:(double_cardinal x) (double_cardinal y) => ha hb. split; last exact: (eq_subset_pr2 ha hb). symmetry in ha; symmetry in hb; exact: (eq_subset_pr2 ha hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)