proposition: Lemma finite_subsets_pr E: finite_subsets_prop E (finite_subsets E) /\ (forall F, finite_subsets_prop E F -> sub (finite_subsets E) F).
proof: Proof. split. rewrite /finite_subsets;split. apply: Zo_i; first by apply /setP_P; fprops. apply: emptyset_finite. move=> x X xE => /Zo_P [] /setP_P XE fX; apply /Zo_i. by apply /setP_P; apply :setU1_sub. by apply: setU1_finite. rewrite /finite_subsets=> F [eF fs] t. move =>/Zo_P [] /setP_P tE fst. apply: (@finite_set_induction1 (fun x=> sub x E)(fun x=> inc x F)) =>//. move => a b h1 h2. apply: fs; first by apply: h2;fprops. apply: h1; apply: (@sub_trans (a +s1 b)) => //;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)