proposition: Lemma Eq_muldl a b c: (dsum b c) \times a \Eq dsum (b \times a) (c \times a).
proof: Proof. apply:(EqT (EqT (Eq_setX2_S (dsum b c) a) (Eq_muldr a b c))). exact:(Eq_sum_inv (Eq_setX2_S a b) (Eq_setX2_S a c)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)