proposition: Lemma starts_withFT_prop l: starts_withFT l = (l == prependFT (drop 2 l)).
proof: Proof. by case:l => // a [ | b l];case: a => //; case:b => //=; rewrite drop0 eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)