proposition: Lemma prod_rel_trans : Transitive R -> Transitive S -> Transitive prod_rel.
proof: Proof. move=> pR pS [a2 b2] [a1 b1] [a3 b3] [??] [??] /=. by split; [apply: (pR a2) | apply: (pS b2)]. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)