proposition: Lemma Exercise4_8b a b: inc a (substrate r) -> inc b (substrate r) -> (E47S r (sup r a b)) = (E47S r a) \cup (E47S r b).
proof: Proof. move=> asr bsr. move: (lattice_sup_pr lr asr bsr)=> [p1 p2 p3]. have isr: inc (sup r a b) (substrate r) by order_tac. have or: order r by move: lr => [ok _]. move: (Exercise4_7k p1) (Exercise4_7k p2) => p4 p5. set_extens t; last first. case /setU2_P => /Zo_P [tsr [si ta]]; apply /Zo_P;split => //; split => //; order_tac. move /Zo_P=> [tsr [si ts]]. by case: (Exercise4_8a dl3 si asr bsr ts)=> le; apply /setU2_P;[left | right]; apply: Zo_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)