proposition: Lemma sublist_lookup_all l n : length l = n → sublist_lookup 0 n l = Some l.
proof: Proof. intros. unfold sublist_lookup; case_guard; [|lia]. by rewrite take_ge by (rewrite drop_length; lia). Qed.
imports: stdpp(options)