proposition: Lemma read_app : forall i l1 l2, (l1 ++ l2)[i] = (If i < length l1 then l1[i] else l2[i - length l1]).
proof: Proof. Proof using IA. intros. rewrite length_eq. unfold read, read_inst, read_impl. case_if. { case_if. { auto. } { false; math. } } case_if as C'. { applys nth_app_l. applys lt_nat_of_lt_int. rewrite abs_nonneg; math. } case_if. { false; math. } rewrite abs_gt_minus_nat; [|math]. applys nth_app_r. { applys ge_nat_of_ge_int. rewrite abs_nonneg; math. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)