proposition: Fact ra_lsum_spec i v lr : Forall2 ⟦f⟧ (map (fun x => x##v) (list_an 0 i)) lr -> ⟦ra_lsum⟧ (i##v) (lsum lr).
proof: Proof. revert lr. induction i as [ | i IHi ]; intros lr H. + simpl in H. apply Forall2_nil_inv_l in H; subst lr; simpl. red; simpl; apply ra_cst_n_val. + replace (S i) with (i+1) in H by lia. rewrite list_an_plus, map_app in H. apply Forall2_app_inv_l in H. destruct H as (l1 & l2 & H1 & H2 & ->). rewrite lsum_app. rewrite Nat.add_comm in H2; simpl in H2. apply Forall2_cons_inv_l in H2. destruct H2 as (yn & l3 & H2 & -> & H3). apply Forall2_nil_inv_l in H3; subst l3. simpl; red; simpl. exists (lsum l1); split. * apply IHi; auto. * apply Hh; exists yn; split; auto; lia. Qed.
imports: Arith List Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list gcd crt sums finite pos vec) Undecidability.MuRec.Util(recalg recomp prim_min)