An Example Equation Problem

Find the roots of `2 sin^2 x = sqrt(3) sin 2x` that are at least `0` and less than `2pi`. equation x=0 \/ x=pi/3 \/ x=pi \/ x=4pi/3 ends /* `x` must be at least `0` and less than `2 pi` */ f_nodes 25 0 <= x < 2pi /\ 2 sin^2 x = sqrt(3) sin 2x /**/
<=> 0 <= x < 2pi /\ 2 sin^2 x = sqrt(3) * 2 sin x cos x /**/ <=> 0 <= x < 2pi /\ ( sin x = 0 \/ sin x = sqrt(3) cos x ) /**/ <=> 0 <= x < 2pi /\ ( x = 0 \/ sin x = sqrt(3) cos x ) /**/ ⇔ 0 ≤ x < 2π ∧ (sin x = 0 ∨ sin^2 x = 3 cos^2 x) /**/ ⇔ 0 ≤ x < 2π ∧ (sin x = 0 ∨ sin^2 x = 3(1 − sin^2 x)) /**/ ⇔ 0 ≤ x < 2π ∧ (sin x = 0 ∨ 4 sin^2 x = 3) /**/ ⇔ 0 ≤ x < 2π ∧ (sin x = 0 ∨ sin x = √(3)/2 ∨ sin x = −√(3)/2 ) /**/ ⇔ x = 0 ∨ x = π ∨ x = π/3 ∨ x = 2π/3 ∨ x = 4π/3 ∨ x = 5π/3 ==> 0 <= x < 2pi /\ ( sin x = 0 \/ sin^2 x = 3 cos^2 x ) /**/ original <=> x = 0 \/ x = pi \/ x = pi/3 \/ x = (4 pi)/3
or