proposition: Lemma strict_sub_smaller y: (forall x, ssub x y -> (cardinal x) <c (cardinal y)) <-> finite_set y.
proof: Proof. split => h. case: (emptyset_dichot y); first by move => ->; apply: emptyset_finite. move=> [a ay]; apply /(finite_set_prop1 ay). exact: (proj2(h _ (setC1_proper ay))). move=> x ssxy. move: (setC_ne ssxy) =>[u uc]. move /setC_P : uc => [uy ux]. move/(finite_set_prop1 uy): h => c1. set (z := y -s1 u). have /sub_smaller lexz: sub x z. apply/subsetC1_P; split => //; exact: (proj1 ssxy). apply: (cle_ltT lexz); split => //; apply: sub_smaller; apply: sub_setC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)