proposition: Lemma Exercise4_7a x: inc x (substrate r) -> sup_irred r x \/ (exists a b, [/\ glt r a x, glt r b x & x = sup r a b]).
proof: Proof. case: (p_or_not_p (sup_irred r x)); first by left. move=> p1; right; ex_middle h; case: p1 => a b asr bsr xs. case: (equal_or_not x a)=> xa; first by left. case: (equal_or_not x b)=> xb; first by right. move: (lattice_sup_pr lr asr bsr); rewrite -xs; move => [p2 p3 _]. by case: h; exists a, b; rewrite /glt;split => //;split => //; apply: nesym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)