proposition: Lemma takeD i j s : take (i + j) s = take i s ++ take j (drop i s).
proof: Proof. elim: i j s => [|i IHi] [|j] [|a s] //; first by rewrite take0 addn0 cats0. by rewrite addSn /= IHi. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)