proposition: Fact ra_prim_max_spec : { e | ⟦ra_prim_max⟧ (a##b##v) e /\ f v e <= b /\ b < f v (S e) }.
proof: Proof. Proof using Hf Hb. exists (prim_min (fun i => S b - f v (S i)) a); split. + unfold ra_prim_max. rewrite ra_prim_min_rel with (f := fun w i => S (vec_head w) - f (vec_tail w) (S i)); auto. intros i w; vec split w with j; simpl vec_tail; simpl vec_head; auto. + destruct prim_min_spec with (f := fun i => S b - f v (S i)) (n := a) as (H2 & H3); try lia. split; try lia. revert H3. destruct (prim_min (fun j => S b - f v (S j)) a) as [ | k ]; intros H3; try lia. specialize (H3 k); 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)