proposition: Lemma Exercise4_8a a: distributive_lattice3 r -> sup_irred r a -> forall x y, inc x (substrate r) -> inc y (substrate r) -> gle r a (sup r x y) -> (gle r a x \/ gle r a y).
proof: Proof. move => dl1 sia x y xsr ysr sa. have or: order r by move: lr => [or _]. have asr: inc a (substrate r) by order_tac. move:(distributive_lattice_prop2 lr) => [_ _ p1]. move: ((p1 dl1) _ _ _ asr xsr ysr); rewrite (inf_comparable1 or sa) => ia. move: (lattice_inf_pr lr asr xsr)(lattice_inf_pr lr asr ysr). move=> [_ px _] [_ py _]. have r1: inc (inf r a x) (substrate r) by order_tac. have r2: inc (inf r a y) (substrate r) by order_tac. by case: (sia _ _ r1 r2 ia); move=> ->; [left | right]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)