diff --git a/RealRooted/Tactic/Examples/HermiteBiehler.lean b/RealRooted/Tactic/Examples/HermiteBiehler.lean
index 155f8730c..7dffd9a23 100644
--- a/RealRooted/Tactic/Examples/HermiteBiehler.lean
+++ b/RealRooted/Tactic/Examples/HermiteBiehler.lean
@@ -35,6 +35,26 @@ example {f g : ℝ[X]}
     imag_pos_lc := hg,
     stable := hstable
 
+example {f g : ℝ[X]}
+    (hf : HasPosLeadingCoeff f) (hg : HasPosLeadingCoeff g)
+    (hstable : IsUpperHalfPlaneStable (hermiteBiehlerPolynomial f g)) :
+    f.Splits ∧ g.Splits := by
+  rr_hermite_biehler_splits using
+    real_pos_lc := hf,
+    imag_pos_lc := hg,
+    stable := hstable
+
+example {f g : ℝ[X]}
+    (hf : HasPosLeadingCoeff f) (hg : HasPosLeadingCoeff g)
+    (hstable : IsUpperHalfPlaneStable (hermiteBiehlerPolynomial f g))
+    (hdegree : 1 ≤ f.natDegree) :
+    Prec g f := by
+  rr_hermite_biehler_prec using
+    real_pos_lc := hf,
+    imag_pos_lc := hg,
+    stable := hstable,
+    real_degree_pos := hdegree
+
 example {p q : ℝ[X]}
     (hp : HasNonnegCoeffs p) (hq : HasNonnegCoeffs q)
     (hstable : IsUpperHalfPlaneStable (hermiteBiehlerPolynomial q p)) :
@@ -74,6 +94,30 @@ example {F G : Nat → ℝ[X]}
     imag_pos_lc := hG,
     stable := hstable
 
+example {F G : Nat → ℝ[X]}
+    (hF : ∀ n : Nat, HasPosLeadingCoeff (F n))
+    (hG : ∀ n : Nat, HasPosLeadingCoeff (G n))
+    (hstable :
+      ∀ n : Nat, IsUpperHalfPlaneStable (hermiteBiehlerPolynomial (F n) (G n))) :
+    ∀ n : Nat, (F n).Splits ∧ (G n).Splits := by
+  rr_hermite_biehler_splits_sequence using
+    real_pos_lc := hF,
+    imag_pos_lc := hG,
+    stable := hstable
+
+example {F G : Nat → ℝ[X]}
+    (hF : ∀ n : Nat, HasPosLeadingCoeff (F n))
+    (hG : ∀ n : Nat, HasPosLeadingCoeff (G n))
+    (hstable :
+      ∀ n : Nat, IsUpperHalfPlaneStable (hermiteBiehlerPolynomial (F n) (G n)))
+    (hdegree : ∀ n : Nat, 1 ≤ (F n).natDegree) :
+    ∀ n : Nat, Prec (G n) (F n) := by
+  rr_hermite_biehler_prec_sequence using
+    real_pos_lc := hF,
+    imag_pos_lc := hG,
+    stable := hstable,
+    real_degree_pos := hdegree
+
 example {P Q : Nat → ℝ[X]}
     (hP : ∀ n : Nat, HasNonnegCoeffs (P n))
     (hQ : ∀ n : Nat, HasNonnegCoeffs (Q n))
diff --git a/RealRooted/Tactic/HermiteBiehler.lean b/RealRooted/Tactic/HermiteBiehler.lean
index 2c7f158f6..6b9865281 100644
--- a/RealRooted/Tactic/HermiteBiehler.lean
+++ b/RealRooted/Tactic/HermiteBiehler.lean
@@ -34,6 +34,23 @@ theorem hermiteBiehlerConverse_sequence {F G : Nat → ℝ[X]}
     ∀ n : Nat, Prec (G n) (F n) ∨ Prec (F n) (G n) :=
   fun n => RealRooted.hermiteBiehlerConverse (hF n) (hG n) (hstable n)
 
+theorem hermiteBiehlerSplits_sequence {F G : Nat → ℝ[X]}
+    (hF : ∀ n : Nat, HasPosLeadingCoeff (F n))
+    (hG : ∀ n : Nat, HasPosLeadingCoeff (G n))
+    (hstable :
+      ∀ n : Nat, IsUpperHalfPlaneStable (hermiteBiehlerPolynomial (F n) (G n))) :
+    ∀ n : Nat, (F n).Splits ∧ (G n).Splits :=
+  fun n => RealRooted.splits_of_stable (hF n) (hG n) (hstable n)
+
+theorem hermiteBiehlerPrec_sequence {F G : Nat → ℝ[X]}
+    (hF : ∀ n : Nat, HasPosLeadingCoeff (F n))
+    (hG : ∀ n : Nat, HasPosLeadingCoeff (G n))
+    (hstable :
+      ∀ n : Nat, IsUpperHalfPlaneStable (hermiteBiehlerPolynomial (F n) (G n)))
+    (hdegree : ∀ n : Nat, 1 ≤ (F n).natDegree) :
+    ∀ n : Nat, Prec (G n) (F n) :=
+  fun n => RealRooted.prec_of_stable_general (hF n) (hG n) (hstable n) (hdegree n)
+
 theorem hermiteBiehlerOddEven_rightHalfPlaneStable_sequence {P Q : Nat → ℝ[X]}
     (hP : ∀ n : Nat, HasNonnegCoeffs (P n))
     (hQ : ∀ n : Nat, HasNonnegCoeffs (Q n))
@@ -74,6 +91,21 @@ syntax (name := rr_hermite_biehler_converse_named)
     "stable" ":=" term :
   tactic
 
+syntax (name := rr_hermite_biehler_splits_named)
+  "rr_hermite_biehler_splits" " using "
+    "real_pos_lc" ":=" term ","
+    "imag_pos_lc" ":=" term ","
+    "stable" ":=" term :
+  tactic
+
+syntax (name := rr_hermite_biehler_prec_named)
+  "rr_hermite_biehler_prec" " using "
+    "real_pos_lc" ":=" term ","
+    "imag_pos_lc" ":=" term ","
+    "stable" ":=" term ","
+    "real_degree_pos" ":=" term :
+  tactic
+
 syntax (name := rr_hermite_biehler_odd_even_hurwitz_named)
   "rr_hermite_biehler_odd_even_hurwitz" " using "
     "odd_nonneg" ":=" term ","
@@ -102,6 +134,21 @@ syntax (name := rr_hermite_biehler_converse_sequence_named)
     "stable" ":=" term :
   tactic
 
+syntax (name := rr_hermite_biehler_splits_sequence_named)
+  "rr_hermite_biehler_splits_sequence" " using "
+    "real_pos_lc" ":=" term ","
+    "imag_pos_lc" ":=" term ","
+    "stable" ":=" term :
+  tactic
+
+syntax (name := rr_hermite_biehler_prec_sequence_named)
+  "rr_hermite_biehler_prec_sequence" " using "
+    "real_pos_lc" ":=" term ","
+    "imag_pos_lc" ":=" term ","
+    "stable" ":=" term ","
+    "real_degree_pos" ":=" term :
+  tactic
+
 syntax (name := rr_hermite_biehler_odd_even_hurwitz_sequence_named)
   "rr_hermite_biehler_odd_even_hurwitz_sequence" " using "
     "odd_nonneg" ":=" term ","
@@ -144,6 +191,21 @@ macro_rules
         stable := $hstable:term) =>
       `(tactic|
         exact RealRooted.hermiteBiehlerConverse $hf $hg $hstable)
+  | `(tactic|
+      rr_hermite_biehler_splits using
+        real_pos_lc := $hf:term,
+        imag_pos_lc := $hg:term,
+        stable := $hstable:term) =>
+      `(tactic|
+        exact RealRooted.splits_of_stable $hf $hg $hstable)
+  | `(tactic|
+      rr_hermite_biehler_prec using
+        real_pos_lc := $hf:term,
+        imag_pos_lc := $hg:term,
+        stable := $hstable:term,
+        real_degree_pos := $hdegree:term) =>
+      `(tactic|
+        exact RealRooted.prec_of_stable_general $hf $hg $hstable $hdegree)
   | `(tactic|
       rr_hermite_biehler_odd_even_hurwitz using
         odd_nonneg := $hp:term,
@@ -175,6 +237,23 @@ macro_rules
       `(tactic|
         exact RealRooted.Tactic.hermiteBiehlerConverse_sequence
           $hf $hg $hstable)
+  | `(tactic|
+      rr_hermite_biehler_splits_sequence using
+        real_pos_lc := $hf:term,
+        imag_pos_lc := $hg:term,
+        stable := $hstable:term) =>
+      `(tactic|
+        exact RealRooted.Tactic.hermiteBiehlerSplits_sequence
+          $hf $hg $hstable)
+  | `(tactic|
+      rr_hermite_biehler_prec_sequence using
+        real_pos_lc := $hf:term,
+        imag_pos_lc := $hg:term,
+        stable := $hstable:term,
+        real_degree_pos := $hdegree:term) =>
+      `(tactic|
+        exact RealRooted.Tactic.hermiteBiehlerPrec_sequence
+          $hf $hg $hstable $hdegree)
   | `(tactic|
       rr_hermite_biehler_odd_even_hurwitz_sequence using
         odd_nonneg := $hp:term,