proposition: Lemma distributive_rec x T: inc x (substrate r) -> sub T (substrate r) -> sup r x (infimum r T) = infimum r (fun_image T (fun z => sup r z x)).
proof: Proof. move: Exercise4_7b => or xsr Tsr. move: (sub_finite_set Tsr fs) => ft; move: T ft Tsr. apply: finite_set_induction0. move=> ok;set im:= fun_image _ _; have ->: im = emptyset. by rewrite /im; apply /set0_P => y /funI_P [z /in_set0]. rewrite Exercise4_8u. move: (the_greatest_pr or Exercise4_7c1) => [_ tlp]. by move: (tlp _ xsr) => aux; apply: (sup_comparable1 or aux). move=> K a hrec naK sKas. have Ksr: sub K (substrate r) by apply: (@sub_trans (K +s1 a)); fprops. have asr: inc a (substrate r) by apply: sKas; fprops. move: (Exercise4_7i1 Ksr) => his. set aux:= fun_image _ _. set K1 := (fun_image K (fun z : Set => sup r z x)). have K1sr:sub K1 (substrate r). move => t /funI_P [z zK ->]. move: (lattice_sup_pr lr (Ksr _ zK) xsr) => [p1 _ _]; order_tac. move: (Exercise4_7i1 K1sr) => K1is. move: (lattice_sup_pr lr asr xsr) => [p1a p2a p3a]. have saxr: inc (sup r a x) (substrate r) by order_tac. have ->: aux = K1 +s1 (sup r a x). set_extens t. move /funI_P => [z zt ->]. case /setU1_P: zt => s; apply /setU1_P; [left |right; ue]. apply /funI_P; ex_tac. case /setU1_P => h; apply /funI_P. move /funI_P: h => [z za zb]; exists z;fprops. rewrite h; exists a;fprops. rewrite (infimum_setU1 lr Ksr his asr) (infimum_setU1 lr K1sr K1is saxr). move: (infimum_pr1 or his) => /(glbP or Ksr) [[p1K p2K] p3K]. move: (distributive_lattice_prop2 lr) => [_ p1 _]. by rewrite ((p1 dl3) _ _ _ xsr p1K asr) (hrec Ksr) -/K1 sup_C. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)