proposition: Lemma constituant_inter2 A B: is_constituant A -> is_constituant B -> intransitive1 -> A = B \/ small_set (A \cap B).
proof: Proof. move=> cA cB i1. case: (equal_or_not A B); first (by left); move => AB;right; move=> u v. case: cA. move=>[a [Aa aE ap]]; rewrite Aa. by move/setI2_P => [/set1_P -> _] /setI2_P [/set1_P -> _]. case: cB. move=>[c [Ac cE cp]] _; rewrite Ac. by move/setI2_P => [_ /set1_P ->] /setI2_P [_ /set1_P ->]. move=> [a [b [Aab nab Rab]]] [a' [b' [Aab' nab' Rab']]]. case: (equal_or_not u v)=>// nuv. rewrite Aab Aab';move => /setI2_P [uA uB] /setI2_P [vA vB]. case: AB; rewrite Aab' Aab. rewrite (Cab_trans nab Rab i1 nuv uB vB). by rewrite (Cab_trans nab' Rab' i1 nuv uA vA). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)