proposition: Lemma refines_prod_R A A' B B' (rA : A -> A' -> Type) (rB : B -> B' -> Type) x y : refines rA x.1 y.1 -> refines rB x.2 y.2 -> refines (prod_R rA rB) x y.
proof: Proof. by rewrite !refinesE => *; apply: prod_RI; split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) CoqEAL(hrel param) ssrmatching