proposition: Fact ra_pred_val n : ⟦ra_pred⟧ (n##vec_nil) (n-1).
proof: Proof. simpl; unfold s_rec. induction n as [ | n IHn ]; simpl. + cbv; trivial. + simpl in IHn; exists (n-1); split; auto. replace (n-0) with n by lia; cbv; 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)