proposition: Lemma Eq_sumA a b c: dsum a (dsum b c) \Eq (dsum (dsum a b) c).
proof: Proof. move: a b c. have aux: (forall u v w a b c, v <> u-> u <> w -> w <> v -> dsum a (dsum b c) \Eq ((a *s1 u) \cup ((b *s1 v) \cup (c *s1 w)))). move=> u v w a b c vu uw wv. rewrite !candu2_rw; apply:Eq_du2; fprops. apply: disjoint_pr; move=> z; move/setX_P => [_ _ /set1_P pa] /setU2_P [] /setX_P [_ _ /set1_P]; rewrite pa => //; apply:nesym => //. apply: Eq_ii1. apply: (EqT (EqS (Eq_indexed ((b *s1 C0) \cup (c *s1 C1)) C1))). by apply:Eq_du2; fprops; apply: Eq_ii1. move: C2_ne_C01 => [/nesym ne3 ne2] a b c. move:(aux _ _ _ a b c C1_ne_C0 ne3 ne2) (aux _ _ _ c a b ne3 ne2 C1_ne_C0 ). rewrite setU2_A setU2_C => s1 s2. exact: (EqT (EqT s1 (EqS s2)) (Eq_sumC c (dsum a b))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)