proposition: Lemma maximal_inclusion s: finite_character s -> nonempty s -> exists x, maximal (sub_order s) x.
proof: Proof. move=>fs nes. have es: inc emptyset s. move: nes=> [x]; rewrite fs=> aux; apply: aux. split; [ fprops | apply: emptyset_finite]. set (E:=union s). have sp: (sub s (\Po E)) by move=> t ts; apply /setP_P; apply: setU_s1. apply: (setP_maximal(A:=s) (F:=E)) =>//. move=> u tou us. rewrite fs; move=> y [ysu fsy]. case: (emptyset_dichot y) => yne; try ue. set(Zy:= fun a => choose (fun b=> inc a b /\ inc b u)). have Zyp: (forall a, inc a y -> (inc a (Zy a) /\ inc (Zy a) u)). move=> a ay; rewrite /Zy; apply choose_pr. by move: (ysu _ ay)=> aux; move: (setU_hi aux) => [v pa pb]; exists v. set (Zz:= fun_image y Zy). have fsZz: (finite_set Zz) by rewrite /Zz; apply: finite_fun_image. move: (sub_osr Zz) => []; set r:=(sub_order Zz) => pa pb. have tor: (total_order r). split => //; rewrite pb /r /ocomparable;move=> a b aZz bZz. have au: (inc a u) by move: aZz => /funI_P [z /Zyp [_ zy] ->]. have bu: (inc b u) by move: bZz => /funI_P [z /Zyp [_ zy] ->]. case: (tou _ _ au bu) =>h; [left | right]; apply /ordo_leP;split => //. have fsr: (finite_set (substrate r)) by ue. have ner: nonempty (substrate r). move: yne=> [w wy]; exists (Zy w) ; rewrite pb; apply /funI_P; ex_tac. move: (finite_set_torder_greatest tor fsr ner) => [x [xsr xgr]]. have ysr: (sub y x). move => t ty. have aux: (inc (Zy t)(substrate r)) by rewrite pb; apply /funI_P; ex_tac. move /ordo_leP: (xgr _ aux). move: (Zyp _ ty)=> [tZ _] [_ _ Zx]; apply: Zx =>//. rewrite fs; move=> z [zy fsz]; move: (sub_trans zy ysr) => zx. move: xsr; rewrite pb; move /funI_P=> [w wy Zyw]. move: (Zyp _ wy); rewrite - Zyw; move => [_ xu]. by move: (us _ xu); rewrite fs; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)