proposition: Lemma take_rev n (T: Type) (s: seq T) : n <= size s -> take n (rev s) = rev (drop (size s - n) s).
proof: Proof. move => h;rewrite -{1}(cat_take_drop (size s - n) s) rev_cat take_size_cat //. by rewrite size_rev size_drop subKn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)