proposition: Lemma prod_rel_func : functional R -> functional S -> functional prod_rel.
proof: Proof. move=> pR pS [a2 b2] [a1 b1] [a3 b3] [R21 S21] [R23 S23] /=. by rewrite (pR _ _ _ R21 R23) (pS _ _ _ S21 S23). Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)