proposition: Lemma Eq_square_mul a b: coarse (a \times b) \Eq (coarse a) \times (coarse b).
proof: Proof. move:(Eq_mulA (a \times b) a b) => ra. move: (Eq_mul_inv (EqS (Eq_mulA a b a)) (EqR b)) => rb. move:(EqT (Eq_mul_inv (EqR a) (Eq_setX2_S b a)) (Eq_mulA a a b)) => rc. move: (EqS (Eq_mulA (coarse a) b b)) => rd. exact:(EqT (EqT (EqT ra rb) (Eq_mul_inv rc (EqR b))) rd). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)