proposition: Lemma Exercise4_8r: r \Is E48APIo.
proof: Proof. pose comp X:= X -s1 (the_least r). pose chrf x := char_fun (comp (E47S r x)) E48P. have ta: lf_axiom chrf (substrate r) E48API. by move=> x xsr;apply: Exercise4_8o. exists (Lf chrf (substrate r) E48API). move: lr => [or _]; move: Exercise4_8k => [_ [p1 p2]]. have chrp: forall u, inc u (substrate r) -> sub (comp (E47S r u)) E48P. move=> u usr; move: (Exercise4_7q usr) => aux t /setC1_P [q1 q2] => //. by apply /setC1_P;split => //; apply: aux. saw. split; aw => //; apply: lf_bijective => //. move => u v usr vsr. move /(char_fun_injectiveP (chrp _ usr) (chrp _ vsr))=> scf. move: (Exercise4_7g usr)(Exercise4_7g vsr) => leu lev. move: (setC1_K leu). rewrite -/(comp (E47S r u)) scf /comp (setC1_K lev) => scf1. move: (f_equal (supremum r) scf1); rewrite Exercise4_7l // Exercise4_7l //. move:Exercise4_8e => [_ p3]. move=> y yf; set U := Vfi1 y \1c. move: yf => /(Exercise4_8iP (Exercise4_7e)) [fy sy ty yp]. have p4: sub U E48P. rewrite - sy /U; apply: sub_inv_im_source => //; rewrite ty. rewrite /E48I;apply: set1_sub; fprops. have p5: (sub U E48P /\ (forall x y, inc y U -> inc x E48P -> gle r x y -> inc x U)). split => // 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. symmetry in wv; rewrite - (yp _ _ xE zy xz wv); apply: Vf_pr3 => //; ue. move: (p3 _ p5) => [x xsr aux]; ex_tac. by rewrite /chrf /comp -aux /U - sy Exercise4_8p. hnf; aw;move=> x y xsr ysr; rewrite !LfV//. move: Exercise4_8g Exercise4_8h => [[q1 q2] [q3 q4]] [q5 q6]. have chrf1: forall x, inc x (substrate r) -> [/\ function (chrf x), source (chrf x) = substrate E48Ps & target (chrf x) = substrate E48Io]. move => z zsr; split; first (by apply: char_fun_f). by rewrite /chrf /char_fun; aw. rewrite /chrf /char_fun; aw; rewrite q6 //. split. move => h; move: (Exercise4_7k h) => h1. move: (chrf1 _ xsr)(chrf1 _ ysr) => [q7 q8 q9] [q10 q11 q12]. have aux: (sub (comp (E47S r x)) (comp (E47S r y))). by move => t /setC1_P [t1 t2]; apply /setC1_P;split => //; apply: h1. move /(Exercise4_8qP (chrp _ xsr) (chrp _ ysr)): aux => hh. by apply /imo_gleP; fprops; split => //; fprops; split => //; rewrite q4. move => h; apply : (Exercise4_7m xsr ysr). move /(imo_gleP _ q5) :h => [_ _ [_ _]]. rewrite q4 => /(Exercise4_8qP (chrp _ xsr) (chrp _ ysr)). move=> aux t t1; case: (equal_or_not t (the_least r)) => tl. by rewrite tl; apply: Exercise4_7g. have t2: inc t (comp (E47S r x)) by apply /setC1_P. by move: (aux _ t2) => /setC1_P []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)