proposition: Fact ra_lsum_S i v : (exists p k, p < i /\ ⟦f⟧ (p##v) (S k)) -> exists k, ⟦ra_lsum⟧ (i##v) (S k).
proof: Proof. Proof using Hf. intros H. assert (forall p : pos i, ex (⟦ f ⟧ (pos2nat p##v))) as H1. { intro; apply Hf'. } apply vec_reif in H1. destruct H1 as (w & Hw). assert (⟦ra_lsum⟧ (i##v) (lsum (vec_list w))) as H1. { apply ra_lsum_spec. rewrite <- pos_list2nat, map_map, map_pos_list_vec. apply Forall2_vec_list. intro; rewrite vec_pos_set; auto. } assert (0 < lsum (vec_list w)) as H2. { destruct H as (p & k & Hp & H2). apply Nat.lt_le_trans with (S k); try lia. apply lsum_le, vec_list_In_iff. exists (nat2pos Hp). specialize (Hw (nat2pos Hp)). rewrite pos2nat_nat2pos in Hw. revert H2 Hw; apply ra_rel_fun. } clear H Hw. revert H1 H2. generalize (lsum (vec_list w)). intros [ | k ]; intros; try lia; exists k; auto. 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)