proposition: Lemma Exercise4_8s: r \Is E48AJImo.
proof: Proof. pose chrf x := char_fun (E47S r x) (irreds r). have ta: lf_axiom chrf (substrate r) (substrate E48AJImo). by move=> x xsr;apply: Exercise4_8n. exists (Lf chrf (substrate r) (substrate E48AJImo)). move: lr => [or _]; move: Exercise4_8k => [[p1 p2] _]. move: Exercise4_8m => [[p3 p4] p5]. have s1: sub (irreds r) (substrate r) by apply: Zo_S. saw. saw; apply: lf_bijective => //. move => u v usr vsr. move /(char_fun_injectiveP (Exercise4_7q usr) (Exercise4_7q vsr))=> scf. move: (f_equal (supremum r) scf); rewrite Exercise4_7l // Exercise4_7l //. move:Exercise4_8d => [_ p6]. move=> y yf; set U := Vfi1 y \1c. move: yf; rewrite p5; move => [aux Wl]; move: aux. move /(Exercise4_8iP s1) => [fy sy ty yp]. have p7: sub U (irreds r). rewrite - sy /U; apply: sub_inv_im_source => //; rewrite ty. rewrite /E48I;apply: set1_sub; fprops. have p8: nonempty U. exists (the_least r); apply /iim_fun_P. exists \1c; [ fprops | rewrite -Wl; apply: Vf_pr3 => // ]. by rewrite sy;apply: Exercise4_7d. have p9: [/\ sub U (irreds r), nonempty U & (forall x y, inc y U -> sup_irred r x -> gle r x y -> inc x U)]. split => //; move=> x z zU xE xz. move: zU => /iim_fun_P [u /set1_P ->] Jg; move: (Vf_pr fy Jg). move: (p1graph_source fy Jg); rewrite sy => zy wv. apply /iim_fun_P;exists \1c; first by fprops. have xE1: inc x (irreds r) by apply: Zo_i => //; order_tac. symmetry in wv;rewrite - (yp _ _ xE1 zy xz wv); apply: Vf_pr3 => //; ue. move: (p6 _ p9) => [x xsr aux]; ex_tac. by rewrite /chrf -aux /U - sy Exercise4_8p. hnf; aw;move=> x y xsr ysr; rewrite !LfV//; rewrite -/(chrf x) -/ (chrf y). move: Exercise4_8g Exercise4_8h => [[q1 q2] [q3 q4]] [q5 q6]. move: (ta _ xsr) (ta _ ysr); rewrite p5 p5; move=> [p6 p7] [p8 p9]. have ta1: lf_axiom (fun _ : Set => \0c) (irreds r) E48I. by rewrite /E48I => t _; fprops. move : Exercise4_7d => aux2. have p10:inc (chrf x) ((substrate E48AJIo) -s1 E48z). apply /setC1_P;split; [ue | move=> h; move: p7; rewrite h / E48z; rewrite LfV//; fprops]. have p11:inc (chrf y) ((substrate E48AJIo) -s1 E48z). apply /setC1_P;split; [ue | move=> h; move: p9; rewrite h / E48z; rewrite LfV//; fprops]. have chrf1: forall x, inc x (substrate r) -> function_prop (chrf x) (substrate E48Js) (substrate E48Io). move => z zsr; split; first by apply: char_fun_f. by rewrite /chrf /char_fun q2; aw. by rewrite /chrf /char_fun q6; aw. split. move: (chrf1 _ xsr)(chrf1 _ ysr) => [q7 q8 q9] [q10 q11 q12]. move => h; apply /iorder_gle0P=> //; apply /(imo_gleP _ q5); split;fprops. split => //. rewrite q2; apply /Exercise4_8qP; try apply: Exercise4_7q => //. exact (Exercise4_7k h). move /iorder_gleP => [pa pb] /(imo_gleP _ q5) [_ _ [_ _]]. rewrite q2; move/(Exercise4_8qP (Exercise4_7q xsr) (Exercise4_7q ysr)). by apply: Exercise4_7m. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)