proposition: Lemma prod_rel_refl : (forall a, R a a) -> (forall b, S b b) -> forall p, prod_rel p p.
proof: Proof. by move=> pR pS [a b] /=. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)