fact: Definition swap_but_first l := if l is a ::s then a:: [seq ~~ x | x <- s] else nil.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)