proposition: Lemma prod_RE A A' B B' (rA : A -> A' -> Type) (rB : B -> B' -> Type) x y : prod_R rA rB x y -> prod_hrel rA rB x y.
proof: Proof. by case; split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) CoqEAL(hrel param) ssrmatching