proposition: Theorem setI_interval r x y: lattice r -> interval r x -> interval r y -> interval r (x \cap y).
proof: Proof. move=> lar ix iy. have or: order r by move: lar=> []. move: (setI_i2 ix) (setI_i2 iy). move=> [a [b [lua rub abx]]][c [d [luc rud cdy]]]. rewrite -abx -cdy setI2_ACA. have lu1: lu_interval r (a \cap c). case: lua. move=>->; rewrite setI2_C setI_i1 //. right; hnf; case: luc; fprops. case: luc. move=>-> p; rewrite setI_i1;[ by right| by right; left]. by move=> p1 p2; right; apply: setI_i3. have ru1: ru_interval r (b \cap d). case: rub. move=>->; rewrite setI2_C setI_i1 //. right; hnf; case: rud; fprops. move=> irub; case: rud. move=>->; rewrite setI_i1 //; [by right | by right; right; left]. move=> irud. move: (opp_osr or) => [ha hb]. have Ha: forall a, interval_cu r a = interval_uc (opp_order r) a. move=> t; set_extens u; move/Zo_P => []; aw => pa pb; apply:Zo_i; try ue; by apply/igraph_pP. have Hb: forall a, interval_ou r a = interval_uo (opp_order r) a. move=> t; set_extens u; move/Zo_P => []; aw; move => pa [p pc]; apply:Zo_i; try ue; split; try (apply/igraph_pP => //); fprops. have Hc: left_unbounded_interval (opp_order r) b. move:irub => [e es be]; case: be => ->; exists e;try ue; fprops. have Hd: left_unbounded_interval (opp_order r) d. move:irud => [e es be]; case: be => ->; exists e; try ue;fprops. have He :lattice (opp_order r) by apply: lattice_opposite. move: (setI_i3 He Hc Hd) => [e es]. rewrite -Ha -Hb; move: es; try ue; move => es//. case => ->; right; exists e; try ue;fprops. have i1: interval r (a \cap c) by right; hnf; case: lu1; fprops. have i2: interval r (b \cap d) by right; hnf; case: ru1; fprops. case: lu1. move=> ->; rewrite setI2_C setI_i1 //. move=> lu2; case: ru1; first by move=>->;rewrite setI_i1 =>//. move=> ru2. left. move: lu2 ru2 => [e es ace][f fs bdf]. case: (p_or_not_p (gle r f e)) => fe. case: ace=> ->. case: bdf=> ->. by left; exists f, e; split => //; zztac2 t; case: pb. by right;right;exists f, e; split => //; left; zztac2 t; case: pb. case: bdf=> ->. by right;right;exists f, e; split => //; right; zztac2 t; case: pb. by right; left ;exists f, e; split => //; zztac2 t; case: pb. suff: (empty ((a \cap c) \cap (b \cap d))). move=> h. move:(empty_interval or fs) => [_ _ oo]; right; left. exists f, f; split => //; try order_tac => //. by set_extens t => te; [ case: (h t) | case: (oo t)]. move=> t /setI2_P [ti1 ti2]; case: fe. have p1: gle r t e. move: ti1; case: ace=> ->; move/Zo_P => [pa pb] //; order_tac. have p2: gle r f t. move: ti2; case: bdf=> ->; move/Zo_P => [pa pb] //; order_tac. order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)