proposition: Lemma refines_split12 : refines (R1 \o R2) x z -> {y : Y & (R1 x y * R2 y z)%type}.
proof: Proof. by rewrite !refinesE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) CoqEAL(hrel param) ssrmatching