proposition: Lemma drop_take_id {A} x (s : seq A) : drop x (take x s) = [::].
proof: Proof. by rewrite -{2}(add0n x) -take_drop take0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)