proposition: Lemma sumt_permt g et : sumt (permt g et) = g (sumt et).
proof: Proof. by elim: et => /= [|e et ->]; rewrite (permc0, permc_addc). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)