proposition: Lemma setI_i3 r x y: lattice r -> left_unbounded_interval r x -> left_unbounded_interval r y -> left_unbounded_interval r (x \cap y).
proof: Proof. move=> lar [a asr xa][b bsr yb]. have or: order r by move: lar=> []. move: (lattice_inf_pr lar asr bsr). set (u:=inf r a b); set (v:= sup r a b). move=> [ua ub uab]. exists u; first by order_tac. case: xa => ->. case: yb => ->. left; zztac2 z; [ by apply:uab | order_tac | order_tac ]. case: (p_or_not_p (glt r u b)). left; zztac2 z; try order_tac; apply: uab => //; order_tac. move=> ltuv; right; zztac2 z; try order_tac. split; first by apply: uab => //; order_tac. by move=> zu; rewrite zu in pd; case: ltuv. move: pb => [pb _]; order_tac. case: yb=> ->. case: (p_or_not_p (glt r u a)) => qe. left; zztac2 z; try order_tac;apply: uab => //; order_tac. right; zztac2 z;try order_tac. split; first by apply: uab => //; order_tac. by move=> zu; rewrite zu in pb; case: qe. move: pb => [pb _]; order_tac. case: (p_or_not_p (glt r u a /\ glt r u b)). move=> [p1 p2]. left; zztac2 z; try order_tac; apply: uab => //; order_tac. move=> p1p2; right; zztac2 z; try order_tac; split. apply: uab => //; order_tac. by move=> zu; rewrite zu in pb pd; case: p1p2; split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)