proposition: Lemma lattice_sup_pr r a b: lattice r -> inc a (substrate r) -> inc b (substrate r) -> [/\ gle r a (sup r a b), gle r b (sup r a b) & forall z, gle r a z -> gle r b z -> gle r (sup r a b) z].
proof: Proof. move=> [or lr] asr bsr. by move: (lr _ _ asr bsr)=> [p1 p2]; apply: sup_pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)