proposition: Lemma prod_RI A A' B B' (rA : A -> A' -> Type) (rB : B -> B' -> Type) x y : prod_hrel rA rB x y -> prod_R rA rB x y.
proof: Proof. by move: x y => [x1 x2] [y1 y2] [] /=; constructor. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) CoqEAL(hrel param) ssrmatching