proposition: Lemma Exercise4_7l u: inc u (substrate r) -> (supremum r (E47S r u)) = u.
proof: Proof. move: Exercise4_7b => or usr. apply: (order_antisymmetry or); first by apply: Exercise4_7j. ex_middle bad. set U := Zo (substrate r) (fun z => ~ gle r z (supremum r (E47S r z))). have neU:nonempty U by exists u; apply: Zo_i. have su: sub U (substrate r) by apply: Zo_S. move: (finite_set_minimal1 su neU) => [t tu tv]. move: (tu) => /Zo_P [tsr bad1]; case: bad1. have sV: sub (E47S r t) (substrate r) by apply: Zo_S. move: (Exercise4_7i sV) => hst. move: (supremum_pr or sV hst) => [[ub1 ub2] _]. case: (Exercise4_7a (su _ tu)) => aux. have h: inc t (E47S r t) by apply: Zo_i => //;split => //; order_tac. by apply: ub2. move: aux => [a [b [[leat neat] [lebt nebt ts]]]]. case: (p_or_not_p (gle r a (supremum r (E47S r a)))); last first. move=> p1;case: neat; apply: tv => //; apply: Zo_i => //; order_tac. case: (p_or_not_p (gle r b (supremum r (E47S r b)))); last first. move=> p1;case: nebt; apply: tv => //; apply: Zo_i => //; order_tac. move=> bs1 bs2. have asr: inc a (substrate r) by order_tac. have bsr: inc b (substrate r) by order_tac. have s1:= (Exercise4_7k leat). have s2:=(Exercise4_7k lebt). have hs1:=(Exercise4_7i (sub_trans s1 sV)). have hs2:=(Exercise4_7i (sub_trans s2 sV)). have le2:=(sup_increasing or (sub_trans s1 sV) sV s1 hs1 hst). have le1:=(sup_increasing or (sub_trans s2 sV) sV s2 hs2 hst). move: (lattice_sup_pr lr asr bsr); rewrite -ts; move=> [h1 h2 h3]. apply: h3; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)