proposition: Lemma take_drop i j s : take i (drop j s) = drop j (take (i + j) s).
proof: Proof. by rewrite addnC; elim: s i j => // x s IHs [|i] [|j] /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)