proposition: Lemma ext_to_prod_identity x y: (identity x) \ftimes (identity y) = identity (x \times y).
proof: Proof. move:(identity_f x) (identity_f y) => fx fy. apply: (function_exten (ext_to_prod_f fx fy) (identity_f (x\times y))). - by rewrite /ext_to_prod; aw. - by rewrite /ext_to_prod; aw. - rewrite {1} /ext_to_prod;aw => i ip /=; rewrite ext_to_prod_V2; aw;trivial. by move /setX_P: (ip) => [ha hb hc]; rewrite !idV; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)