Theory Aux_Sturm_Calculation

section ‹‹Aux_Sturm_Calculation› -- Auxiliary theory for technical reasons.›

theory Aux_Sturm_Calculation imports
  Sturm_Sequences.Sturm
begin

text ‹We prove this fact in a separate theory because in ‹Collision.thy›,
  the @{method sturm} method fails with an internal error.›
lemma sturm_calculation: ‹12 * (r⇧2+154)^3 - (10/3 * (r+2)^3 + 20)⇧2 ≠ 0› if ‹r ≥ 0› for r :: real
  by sturm

end