proposition: Lemma inl_prod_uu_prop:inl_map2_compat inl_prod_SEE inl_prod_SFF inl_prod_uu.
proof: Proof. rewrite /inl_prod_uu; split; aww. move => i /= iI; rewrite LgV // /inl_product_E. have qa: inc i (isI SF) by rewrite - (inl_same_index_same_I si2). have qb: inc i (isI SE') by rewrite - (inl_same_index_same_I si1). move:(proj43 cu _ iI) (proj43 cu' _ qb) => fpa fpb. by rewrite !LgV //; apply:ext_to_prod_fun_bis. move => i j /= leij. move:(inl_prop0 leij) => [iI jI]. have ha: inc (J i j) (isr SF) by rewrite - si2. have hb: inc (J i j) (isr SF') by rewrite - si3. have hc: inc (J i j) (isr SE') by rewrite - si1. move:(inl_prop0 hc) => [iI' jI']. rewrite /inl_product_f !LgV //. move:(inl_prop4 leij)(inl_prop4 hc)(inl_prop4 ha)(inl_prop4 hb) => h1 h2 h3 h4. move:(proj43 cu _ iI) (proj43 cu _ jI) => fpui fpuj. move:(proj43 cu' _ iI') (proj43 cu' _ jI') => fpui' fpuj'. move:(proj44 cu _ _ leij) (proj44 cu' _ _ hc) => uv1 uv2. rewrite (ext_to_prod_comp_bis fpui fpui' h3 h4). by rewrite uv1 uv2 (ext_to_prod_comp_bis h1 h2 fpuj fpuj'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)