proposition: Lemma lookup_insert_old: forall A x y (o : option A) e, x > y -> lookup x (raw_insert y o e) = lookup (x - 1) e.
proof: Proof. induction x; intros; [ elimtype False; lia | replace (S x - 1) with x by lia ]. - { destruct y; destruct e; simpl; try solve [ eauto ]. - rewrite lookup_empty_None. erewrite <- lookup_empty_None. intuition. - destruct x; intros; [ elimtype False; lia | replace (S x - 1) with x in * by lia ]. simpl lookup at 2. intuition. } Qed.
imports: List Arith Lia Dblib(DblibTactics DeBruijn)