proposition: Lemma size_take_and_drop (A : Type) t d n (s : seq A) : n.-1 * d + t <= size s -> size (take_and_drop t d n s) = n * t.
proof: Proof. elim: n s => [/= //|/= [|n] IH s tLs]; rewrite ?addn0 in tLs. rewrite size_cat size_take addn0 mul1n; case: ltngtP => //. by rewrite ltnNge tLs. rewrite size_cat size_take IH; last first. rewrite size_drop leq_subRL; first by rewrite addnA. by rewrite (leq_trans _ tLs) // mulSn -addnA leq_addr. case: ltngtP => [||<-] //. by rewrite ltnNge (leq_trans _ tLs) // leq_addl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)