proposition: Lemma setI_i2 r x: interval r x -> (exists u v, [/\ lu_interval r u, ru_interval r v & u \cap v = x]).
proof: Proof. move=> ix; move: (ix). have p1: forall b, inc b (substrate r) -> lu_interval r (interval_uc r b). by move=> b hb; right; exists b => //; left. have p2: forall b, inc b (substrate r) -> lu_interval r (interval_uo r b). by move=> b hb; right; exists b => //; right. have p3: forall b, inc b (substrate r) -> ru_interval r (interval_cu r b). by move=> b hb; right; exists b => //; left. have p4: forall b, inc b (substrate r) -> ru_interval r (interval_ou r b). by move=> b hb; right; exists b => //; right. case. case. move=> [a [b [au bu ab xab]]]. exists (interval_uc r b), (interval_cu r a); split; fprops. by rewrite xab; zztac2 y; case :pb. case. move=> [a [b [au bu ab xab]]]. exists (interval_uo r b), (interval_ou r a); split; fprops. by rewrite xab; zztac2 y; case: pb. move=> [a [b [au bu ab xab]]]. case: xab=> ->. exists (interval_uc r b), (interval_ou r a); split; fprops. by zztac2 y; case: pb. exists (interval_uo r b), (interval_cu r a); split; fprops. by zztac2 y; case: pb. case. move=>[a au xa]. exists x, (interval_uu r);split. + by case: xa => ->; fprops. + by left. + by apply: setI_i1. case. move=>[a au xa]. exists (interval_uu r), x; split. + by left. + case: xa => ->; fprops. + by rewrite setI2_C; apply: setI_i1. move=> h; exists x, x; rewrite h. split; try (left => //);apply: setI_i1; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)