proposition: Lemma insert_insert: forall A k s (a b : option A) e, k <= s -> raw_insert k a (raw_insert s b e) = raw_insert (1 + s) b (raw_insert k a e).
proof: Proof. intros ? k s. generalize s k; clear s k. induction s; intros. - destruct k; [ | elimtype False; lia ]. reflexivity. - { destruct k. - reflexivity. - destruct e; replace (1 + S s) with (S (1 + s)) by lia; simpl; f_equal; intuition. } Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)