proposition: Lemma Eq_muldr a b c: a \times dsum b c \Eq dsum (a \times b) (a \times c).
proof: Proof. rewrite ! candu2_rw set2_UXr; apply: Eq_du2; try apply:Eq_mulA. apply: disjointU2_pr0;apply: disjointU2_pr; fprops. apply: (disjointU2_pr); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)