proposition: Theorem empty_take n s : empty s -> empty (take n s).
proof: Proof. revert s; elim n; simpl; auto. - intros s; case s; auto. intros n1 l1 _ p; apply empty_nil. - intros n1 Rec s; case s; auto. intros n2 s1 H. case empty_inv with (1 := H); intros H1 H2; subst. apply empty_cons; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia