proposition: Lemma zprod_singleton M r: ~ inc r M -> let N := zprod2 M (singleton r) in ( (forall u, inc u M -> inc (doubleton u r) N) /\ (forall x, inc x N -> exists2 u, inc u M & x = doubleton u r)).
proof: Proof. move=> nrM N; split. move=> u uM; apply /zprod2_P;split => //. move=> t /set2_P; case => ->; apply /setU2_P; [left | right]; fprops. exists u; apply: set1_pr; first by fprops. by move=> t /setI2_P [] /set2_P; case => // ->. exists r; apply /intersection_singletonP;fprops. move=> x xN; move: (zprod2_pr0 xN) => [pa /set1_P <- _ _]. by ex_tac; exact: (zprod2_pr2 xN). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)