proposition: Lemma prod_rel_pre_sym : pre_Symmetric R -> pre_Symmetric S -> pre_Symmetric prod_rel.
proof: Proof. by rewrite !sym_iff_pre_sym; apply: prod_rel_sym. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)