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