proposition: Lemma constitutant_inter3 A B C: is_constituant A -> is_constituant B -> is_constituant C -> intransitive1 -> A = B \/ A = C \/ B = C \/ A \cap B = emptyset \/ A \cap C = emptyset \/ B \cap C = emptyset \/ (A \cap B = A \cap C /\ B \cap C = A \cap C).
proof: Proof. move=> cA cB cC i1. case: (equal_or_not A B); [by left| move=> nAB; right]. case: (equal_or_not A C); [by left| move=> nAC; right]. case: (equal_or_not B C); [by left| move=> nBC; right]. have ssAB: small_set (A \cap B). by case: (constituant_inter2 cA cB i1). have ssAC: small_set (A \cap C). by case: (constituant_inter2 cA cC i1). have ssBC: small_set (B \cap C). by case: (constituant_inter2 cB cC i1). case: cA. move=> [a [Aa aE ap]]; case cB. move=> [b [Bb bE bp]]. left; apply: disjoint_pr=> u ua ub; case: nAB. by move: ua ub;rewrite Aa Bb; move /set1_P => -> /set1_P ->. move => [b1 [b2 [Bbb nbb Rbb]]]. left; apply: disjoint_pr => u; rewrite Aa Bbb; move /set1_P => ->. move/Zo_hi=> [R1 R2]; case: nbb. by rewrite -(ap _ (A2 R1)) (ap _ (A2 R2)). move => [a1 [a2 [Aaa naa Raa]]]. case: cB. move=> [b [Bb bE bp]]; case: cC. move=> [c [Cc cE cp]]. right;right;left; apply: disjoint_pr=> u; rewrite Bb Cc; move /set1_P=> ->. by move/set1_P=> bc; case nBC;rewrite Bb Cc bc. move => [c1 [c2 [Ccc ncc Rcc]]]. right; right;left; apply: disjoint_pr => u; rewrite Bb Ccc; move/set1_P=> ->. by move /Zo_hi=> [R1 R2]; case ncc; rewrite -(bp _ (A2 R1)) (bp _ (A2 R2)). move => [b1 [b2 [Bbb nbb Rbb]]]. case: cC. move=> [c [Cc cE cp]]. right;left;apply: disjoint_pr => u uA uC; move: uC uA; rewrite Aaa Cc. move /set1_P=> -> /Zo_hi [R1 R2]; case: naa. by rewrite -(cp _ (A2 R1)) (cp _ (A2 R2)). move => [c1 [c2 [Ccc ncc Rcc]]]. case: (emptyset_dichot (A \cap B));[ by left | move=> [c ci]; right]. case: (emptyset_dichot (A \cap C));[ by left | move=> [b bi]; right]. case: (emptyset_dichot (B \cap C));[ by left | move=> [a ai]; right]. have iAB: A \cap B = singleton c by apply: set1_pr2. have iAC: A \cap C = singleton b by apply: set1_pr2. have iBC: B \cap C = singleton a by apply: set1_pr2. rewrite iAB iAC iBC. suff: (inc c C). move=> cC. have cAC: inc c (A \cap C) by move/setI2_P: ci => []; fprops. have cBC: inc c (B \cap C) by move/setI2_P: ci => []; fprops. by rewrite (ssAC _ _ bi cAC) (ssBC _ _ ai cBC). case: (equal_or_not a b). move=> ab. have: inc a (A \cap B). apply setI2_i; [by rewrite ab;apply: (setI2_1 bi) | apply: (setI2_1 ai)]. rewrite iAB; move /set1_P => <-; apply: (setI2_2 ai). move=> nab. move: ai bi ci => /setI2_P [aB aC] /setI2_P [bA bC] /setI2_P [cA cB]. move: cA cB bA bC aB aC; rewrite Aaa Bbb Ccc. move => /Zo_P [cE [Ra1c Ra2c]] /Zo_hi [Rb1c Rb2c]. move => /Zo_hi [Ra1b Ra2b] /Zo_hi [Rc1b Rc2b]. move => /Zo_hi [Rb1a Rb2a] /Zo_hi [Rc1a Rc2a]. move: (i1 _ _ _ _ ncc Rcc Rc1a Rc1b Rc2a Rc2b) => Rab. move: (i1 _ _ _ _ nbb Rbb Rb1a Rb1c Rb2a Rb2c) => Rac. move: (i1 _ _ _ _ naa Raa Ra1b Ra1c Ra2b Ra2c) => Rbc. move: (i1 _ _ _ _ nab Rab (A2 Rc1a) Rac (A2 Rc1b) Rbc) => Rc1c. move: (i1 _ _ _ _ nab Rab (A2 Rc2a) Rac (A2 Rc2b) Rbc) => Rc2c. by apply: Zo_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)