proposition: Lemma equivalence_partition_gt1P (T : finType) (R : rel T) (D : {set T}) : {in D & &, equivalence_rel R} -> reflect (exists x y, [/\ x \in D, y \in D & ~~ R x y]) (1 < #|equivalence_partition R D|).
proof: Proof. move => E. set P := equivalence_partition R D. have EP : partition P D by apply: equivalence_partitionP. apply: (iffP card_gt1P). - move => [B1] [B2] [A B C]. have ?: set0 \notin P by case/and3P: EP. case: (set_0Vmem B1) => [?|[x1 inB1]]; first by subst; contrab. case: (set_0Vmem B2) => [?|[x2 inB2]]; first by subst; contrab. have ? : x1 \in cover P. { apply/bigcupP. by exists B1. } have ? : x2 \in cover P. { apply/bigcupP. by exists B2. } exists x1; exists x2. split; rewrite -?(cover_partition EP) //. have TP : trivIset P by case/and3P : EP. apply:contraNN C => Rxy. rewrite -(def_pblock TP A inB1) -(def_pblock TP B inB2) eq_pblock //. by rewrite pblock_equivalence_partition // -?(cover_partition EP). - move => [x] [y] [A B C]. exists (pblock P x). exists (pblock P y). rewrite !pblock_mem ?(cover_partition EP) //. split => //. rewrite eq_pblock ?(cover_partition EP) //; last by case/and3P : EP. by rewrite pblock_equivalence_partition. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)