proposition: Lemma ext_to_prod_coP f g f' g': g \coP f -> g' \coP f' -> (g \ftimes g') \coP (f \ftimes f').
proof: Proof. move => [ha hb hc][ra rb rc]; split => //. - by apply:ext_to_prod_f. - by apply:ext_to_prod_f. - by rewrite /ext_to_prod; aw; rewrite hc rc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)