proposition: Lemma take_seq j n m : take m (seq j n) = seq j (m `min` n).
proof: Proof. revert j m. induction n as [|n IH]; simpl; intros j m. - rewrite take_nil. replace (m `min` 0) with 0 by lia. done. - destruct m; simpl; auto with f_equal. Qed.
imports: stdpp(options)