proposition: Lemma nth_take_and_drop (A : Type) (a : A) t d m n s : 0 < t <= d -> m < n * t -> n.-1 * d + t <= size s -> nth a (take_and_drop t d n s) m = nth a s ((m %/ t) * d + m %% t).
proof: Proof. move=> /andP[t_gt0 tLd]. elim: n m s => //= n IH m s mLtd tdLs. have tLs : t <= size s. by rewrite (leq_trans _ tdLs) // leq_addl. rewrite nth_cat size_take_min (minn_idPl _) //. case: leqP => [tLm|mLt]; last first. by rewrite divn_small // add0n modn_small // nth_take. rewrite {}IH //. - rewrite nth_drop -{3 4}(subnK tLm). by rewrite divnDr ?divnn // t_gt0 addn1 mulSn addnA modnDr. - by rewrite ltn_subLR. case: n mLtd tdLs => [|n mLtd tdLs]; first by rewrite mul1n ltnNge tLm. rewrite size_drop leq_subRL //=; first by rewrite addnA -mulSn. by apply: leq_trans tdLs; rewrite mulSn -addnA leq_addr. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)