proposition: Fact ra_pred_rel v e : ⟦ra_pred⟧ v e <-> e = vec_head v - 1.
proof: Proof. vec split v with n; vec nil v; simpl. split. + intros H. apply ra_rel_fun with (1 := H) (2 := ra_pred_val _). + intros; subst; apply ra_pred_val. 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)