proposition: Lemma swap_but_last_size l: size (swap_but_last l) = size l.
proof: Proof. rewrite /swap_but_last -{2} (revK l) 2!size_rev. by case: (rev l) => // a b; rewrite /swap_but_first /= size_map. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)