proposition: Lemma ra_dio_poly_find_rel_strong1 w e : ⟦ra_dio_poly_find⟧ w e -> ⟦ra_dio_poly_test p q⟧ (e ##w) 0.
proof: Proof. simpl; unfold s_min. intros [H1 H2]. eauto. 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)