proposition: Fact ra_lsum_0 i v : (forall p, p < i -> ⟦f⟧ (p##v) 0) -> ⟦ra_lsum⟧ (i##v) 0.
proof: Proof. intros H. assert (lsum (map (fun _ => 0) (list_an 0 i)) = 0) as E. { clear v H; generalize 0 at 2; induction i; intros j; simpl; auto. } rewrite <- E. apply ra_lsum_spec. rewrite Forall2_map_left, Forall2_map_right, Forall2_Forall, Forall_forall. intros p; rewrite list_an_spec; intros Hp; apply H; 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)