proposition: Lemma prod_rel_sym : Symmetric R -> Symmetric S -> Symmetric prod_rel.
proof: Proof. by move=> pR pS [a1 b1] [a2 b2] /=; rewrite pR pS. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)