proposition: Lemma prod_rel_asym : Antisymmetric R -> Antisymmetric S -> Antisymmetric prod_rel.
proof: Proof. move=> pR pS [a1 b1] [a2 b2] [R12 S12] [R21 S21]. by rewrite (pR _ _ R12 R21) (pS _ _ S12 S21). Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)