proposition: Lemma Eq_sum_inv A B C D: A \Eq B -> C \Eq D -> dsum A C \Eq dsum B D.
proof: Proof. move:C0_ne_C1 C1_ne_C0 => ha hb sa sb; rewrite ! candu2_rw. by apply: Eq_du2; fprops; apply:Eq_ii2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)