proposition: Lemma card'_perm (T : eqType) (s s' : seq T) (P : pred T) : perm_eq s s' -> card' s P = card' s' P :> nat.
proof: Proof. move=> peq_ss'; rewrite /card' /size_op !size_seqE. by apply/perm_size/seq.permP=> x; rewrite !count_filter; apply/seq.permP. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop binomial finset finfun zmodp ssralg countalg finalg poly polydiv) mathcomp(perm fingroup) CoqEAL(hrel pos param refinements binnat boolF2 seqpoly poly_op trivial_seq poly_div boolF2)