proposition: Lemma intersection_sub1 A B C: A = union2 B C -> (forall x, inc x C -> exists y, inc y B /\ sub y x) -> intersection A = intersection B.
proof: Proof. move=> -> h. case: (emptyset_dichot B) => bne. rewrite bne set0_U2. have -> //: C = emptyset. by apply /set0_P => t /h [y []]; rewrite bne => /in_set0. have neA: nonempty (B \cup C). by move: bne => [x xB]; exists x; apply /setU2_P; left. set_extens t. move /(setI_P neA) => aux; apply /(setI_P bne) => i iB; apply: aux; fprops. move /(setI_P bne) => aux; apply /(setI_P neA) => i iB. case/setU2_P: iB => iB; first by apply: aux. by move: (h _ iB) => [y [yB]]; apply; apply: aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)