proposition: Lemma Exercise4_7o a b: inc a (substrate r) -> inc b (substrate r) -> (E47S r (inf r a b)) = (E47S r a) \cap (E47S r b).
proof: Proof. move=> asr bsr. move: (lattice_inf_pr lr asr bsr)=> [p1 p2 p3]. have isr: inc (inf r a b) (substrate r) by order_tac. move: (Exercise4_7k p1) (Exercise4_7k p2) => p4 p5. set_extens t; first by move=> t1; apply /setI2_P; split; fprops. move => /setI2_P [] /Zo_P [tsr [si ta]] /Zo_hi [_ tb]; apply /Zo_P;split;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)