proposition: Lemma insert_insert_always: forall A k s (a b : option A) e, raw_insert k a (raw_insert s b e) = raw_insert (shift k s) b (raw_insert (if le_gt_dec k s then k else k - 1) a e).
proof: Proof. intros. destruct (le_gt_dec k s). - rewrite lift_idx_old by assumption. eauto using insert_insert. - rewrite lift_idx_recent by assumption. replace k with (1 + (k - 1)) in * by lia. rewrite <- insert_insert by lia. do 2 f_equal. lia. Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)