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