proposition: Fact ra_dio_poly_test_total : total ⟦ra_dio_poly_test⟧.
proof: Proof. apply prim_rec_tot, ra_dio_poly_test_prim. Qed.
imports: List Arith Undecidability.Shared.Libs.DLW(utils_tac utils_nat pos vec) Undecidability.MuRec.Util(recalg ra_utils recomp ra_recomp) Undecidability.H10.Dio(dio_single)