proposition: Lemma zprod2_pr1a a b x z: inc x (zprod2 a b) -> inc z a -> inc z x -> z = zpr x a.
proof: Proof. move=> xz za zb; apply/set1_P;move: (zprod2_pr1 xz)=> [<- _]; fprops. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)