proposition: Lemma alter_app_r_alt f l1 l2 i : length l1 ≤ i → alter f i (l1 ++ l2) = l1 ++ alter f (i - length l1) l2.
proof: Proof. intros. assert (i = length l1 + (i - length l1)) as Hi by lia. rewrite Hi at 1. by apply alter_app_r. Qed.
imports: stdpp(options)