proposition: Lemma length_delete l i : is_Some (l !! i) → length (delete i l) = length l - 1.
proof: Proof. rewrite lookup_lt_is_Some. revert i. induction l as [|x l IH]; intros [|i] ?; simpl in *; [lia..|]. rewrite IH by lia. lia. Qed.
imports: stdpp(options)