proposition: Lemma zequiv_no_graph M: nonempty M -> ~ (exists S, forall M', ziequivalent M M' -> inc M' S).
proof: Proof. move=> nM [S hs]. move: (zequiv_example4 M (union S)) => [M' [ds emm']]. move: (hs _ emm') => ms'. case: (emptyset_dichot M') => me. rewrite me in emm'; move: (zequiv_empty emm') => em. by move: nM; rewrite em; case /nonemptyP. move: me => [x xm]; empty_tac1 x; union_tac. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)