proposition: Lemma Exercise4_8e: let comp:= fun X => X -s1 (the_least r) in let p:= fun U => (sub U E48P /\ (forall x y, inc y U -> inc x E48P -> gle r x y -> inc x U)) in (forall x, inc x (substrate r) -> p (comp (E47S r x))) /\ (forall U, p U -> exists2 x, (inc x (substrate r)) & U = comp (E47S r x)).
proof: Proof. move: Exercise4_7b Exercise4_8d => or [pa pb] comp p; split. move=> x xsr; move: (pa _ xsr) => [p1 p2 p3]; split. move => t /setC1_P [p4 p5]; apply /setC1_P;split;fprops. move=> z y /setC1_P [yE yne] /setC1_P [zi znl] zy;apply/setC1_P;split=> //. move: zi => /Zo_P [_ zi]; apply: (p3 _ _ yE zi zy). move=> U [p1 p2]. set U' := U +s1 (the_least r). have [x xsr aux]:exists2 x, inc x (substrate r) & U' = E47S r x. apply: (pb U'); split => //. move=> t; case /setU1_P; last by move => ->; apply: Exercise4_7d. by move=> tu; move: (p1 _ tu) => /setC1_P []. by exists (the_least r); rewrite /U';fprops. move=> x y yU' ir xy; apply /setU1_P. have xsr: inc x (substrate r) by order_tac. case: (equal_or_not x (the_least r)) ; [ by right | move => nxle; left]. have xp: inc x E48P by apply /setC1_P;split => //; apply: Zo_i. move: yU' => /setU1_P; case. by move=> yU; move: (p2 _ _ yU xp xy). move: (the_least_pr or Exercise4_7c) => [_ tle]. move=> h; rewrite h in xy; case: nxle; move: (tle _ xsr) => aux; order_tac. ex_tac. rewrite -aux; set_extens t. move => tu; apply /setC1_P; split => //; first by apply /setU1_P; left. by move: (p1 _ tu) => /setC1_P []. move /setC1_P => [] /setU1_P; case => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)