proposition: Lemma strict_sub_smaller_contra x y: finite_set y -> sub x y -> cardinal x = cardinal y -> x = y.
proof: Proof. move => /strict_sub_smaller ha hb hc; ex_middle bad. by case: (proj2 (ha _ (conj hb bad))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)