proposition: Lemma finite_union2 x y: finite_set x -> finite_set y -> finite_set (x \cup y).
proof: Proof. move=> fsx fsy. set (E:=x \cup y). set (t:= Zo (\Po E) (fun a=> finite_set (x \cup a))). suff: (inc y t) by move /Zo_P; rewrite -/E; case. have yf:inc y (finite_subsets E). apply: Zo_i => //; apply /setP_P => s su; rewrite/E; fprops. suff h: (finite_subsets_prop E t). by move: (finite_subsets_pr E) => [h1 h2]; apply: (h2 _ h). split. rewrite /t; apply: Zo_i; first by apply /setP_P; fprops. by rewrite setU2_0. move=> z X zE => /Zo_P [] /setP_P XE fsu; apply: Zo_i. by apply /setP_P; apply : setU1_sub. by rewrite setU2_A; apply: setU1_finite. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)