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