proposition: Lemma Exercise1_17e r x y: boolean_lattice r -> complete_lattice r -> inc y (substrate r) -> sub x (substrate r)-> inf r y (supremum r x) = supremum r (fun_image x (fun z => inf r y z)).
proof: Proof. move=> blr [or clr] ysr xsr. move: (blr) => [[lr _ _] _ _]. move: (clr _ xsr) => [hsx _]. move: (supremum_pr1 or hsx) => /(lubP or xsr) [[sxs sxu] sxp]. move: (lattice_inf_pr lr ysr sxs). set (v:= inf r y (supremum r x)); move => [p1 p2 p3]. set Y:= fun_image x _. have sY: sub Y (substrate r). move => t /funI_P [z zx ->]. move:(lattice_inf_pr lr ysr (xsr _ zx)) => [h _ _]; order_tac. move: (clr _ sY) => [hsy _]. move: (supremum_pr1 or hsy) => /(lubP or sY). set (u:= supremum r Y);move=> [[sus syu] syp]. set ys:= (standard_completion r y). have leuv: gle r u v. apply: syp; split; first (by order_tac); move=> t /funI_P [z zx ->]. move:(lattice_inf_pr lr ysr (xsr _ zx)) => [h1 h2 h3]. apply: p3 => //; move: (sxu _ zx) => zs; order_tac. have le1: gle r u y by order_tac. have <-:(inf r y (sup r ys u) = u). by rewrite (proj41 (Exercise1_17d blr sus ysr)) inf_C; apply: inf_comparable1. rewrite /v - (proj41 (Exercise1_17d blr sxs ysr)). apply: f_equal. move: (proj31 (scompl_pr blr ysr)); rewrite -/ys=> q1. move: (lattice_sup_pr lr q1 sxs) (lattice_sup_pr lr q1 sus). set z:= (sup r ys u); set z' :=(sup r ys (supremum r x)). move=>[r1 r2 r3] [r4 r5 r6]. apply: (order_antisymmetry or). apply: r3; first (by exact); apply: sxp; split; first by order_tac. move => t tx. have iyt: inc (inf r y t) Y by apply /funI_P; ex_tac. move: (sup_monotone lr q1 (syu _ iyt)). move: (Exercise1_17d blr (xsr _ tx) ysr) =>[_ _ _ aux ]. rewrite /ys aux -/ys -/z => le4. move: (lattice_sup_pr lr q1 (xsr _ tx)) => [_ le5 _]; order_tac. apply: r6; first (by exact); apply: syp; split; first by order_tac. move=> t /funI_P [s sx ->]. have le2:=(proj32 (lattice_inf_pr lr ysr (xsr _ sx))). have le3 := (proj32 (lattice_sup_pr lr q1 sxs)). apply: (order_transitivity or le2 (order_transitivity or (sxu _ sx) le3)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)