proposition: Lemma reverse_drop l n : reverse (drop n l) = take (length l - n) (reverse l).
proof: Proof. rewrite take_reverse. destruct (decide (n ≤ length l)). - repeat f_equal; lia. - by rewrite !drop_ge by lia. Qed.
imports: stdpp(options)