proposition: Lemma finite_character_example r: order r -> finite_character(Zo (\Po (substrate r)) (fun z => total_order (induced_order r z))).
proof: Proof. move=> or s; split. move /Zo_P => [] /setP_P sr tor y [ys fsy];apply: Zo_i. have sys: (sub y (substrate r)) by apply: sub_trans sr. by apply /setP_P. have ->: (induced_order r y) = (induced_order (induced_order r s) y). by rewrite iorder_trans. apply: total_order_sub =>//; rewrite iorder_sr//. move=> h. have p1: sub s (substrate r). move=> t ts; set (y:= singleton t). have p1: (sub y s) by rewrite/y; apply: set1_sub. have p2: (finite_set y) by rewrite /y; apply: set1_finite. have p3: (sub y s /\ finite_set y) by split => //. move: (h _ p3) => /Zo_P [] /setP_P ysr _. apply: ysr; rewrite /y; fprops. apply: Zo_i; first by apply /setP_P. move: (iorder_osr or p1) => [pa pb]. split => //; rewrite pb. move=> x y xs ys; rewrite /ocomparable. set (z:= doubleton x y). have p2: (sub z s /\ finite_set z). by split; rewrite /z; [ apply: sub_set2 |apply: set2_finite]. move: (h _ p2) => /Zo_P [] /setP_P zsr [oz]; rewrite iorder_sr // => toz. case: (toz _ _ (set2_1 x y) (set2_2 x y)) => h1; [left | right]; apply /iorder_gle0P => //; exact: (iorder_gle1 h1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)