proposition: Lemma insert_app_r_alt l1 l2 i x : length l1 ≤ i → <[i:=x]>(l1 ++ l2) = l1 ++ <[i - length l1:=x]>l2.
proof: Proof. intros. assert (i = length l1 + (i - length l1)) as Hi by lia. rewrite Hi at 1. by apply insert_app_r. Qed.
imports: stdpp(options)