proposition: Lemma Eq_mul_inv A B C D: A \Eq B -> C \Eq D -> (A \times C) \Eq (B \times D).
proof: Proof. move => [f [bf <- <-]] [f' [bf' <- <-]]. move:(ext_to_prod_fb bf bf') => h. by exists (f \ftimes f'); split => //; rewrite /ext_to_prod; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)