proposition: Lemma setN01E (T : finType) A (x:T) : A != set0 -> A != [set x] -> exists2 y, y \in A & y != x.
proof: Proof. case/set0Pn => y Hy H1; apply/exists_inP. apply: contraNT H1 => /exists_inPn => H; apply/eq_set1P. suff S: {in A, all_equal_to x} by rewrite -{1}(S y). by move => z /H /negPn/eqP. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)