proposition: Lemma split_rev (T: Type) (a:T) l: rev (a :: l) = last a l :: behead (rev (a :: l)).
proof: Proof. by rewrite rev_cons {1} headI head_rev. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)