proposition: Lemma Exercise4_7m a b: inc a (substrate r) -> inc b (substrate r) -> sub (E47S r a) (E47S r b) -> gle r a b.
proof: Proof. move => asr bsr sab. set E := (E47S r a). have sE: sub E (substrate r) by apply: Zo_S. move: (sub_finite_set sE fs) => fsE. rewrite - (Exercise4_7l asr). apply /(lattice_finite_sup3P lr _ fsE (Exercise4_7h asr) sE). by move=> z zE; move: (sab _ zE) =>/Zo_hi [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)