proposition: Lemma swap_but_last_nil l: nilp (swap_but_last l) = nilp l.
proof: Proof. by rewrite /nilp swap_but_last_size. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)