proposition: Lemma zmap_example4 M r: let N := zprod2 M (singleton r) in ~ (inc r M) -> disjoint M N -> ziequivalent M N.
proof: Proof. move=> N h1 h2. move: (zprod_singleton h1) => [pa pb]. suff : (zbijective (fun x => doubleton x r) M N) by apply: (zmap_example3 h2). split => //. move=> x x' xM xM' sf. have : (inc x (doubleton x r)) by fprops. rewrite sf;case /set2_P => // aux;case: h1; ue. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)