proposition: Lemma perm_sumn s1 s2 : perm_eq s1 s2 -> sumn s1 = sumn s2.
proof: Proof. by apply/catCA_perm_subst: s1 s2 => s1 s2 s3; rewrite !sumn_cat addnCA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)