4(x-9) = 9 + 6 sqrt(x) + x /\ x >= 9 /**/
<=> 3x - 45 = 6 sqrt(x) /\ x >= 9 /**/
<=> x - 15 = 2 sqrt(x) /\ x >= 9 /**/
<=> x^2 - 30x + 225 = 4x /\ x >= 15 /**/
<=> x^2 - 34x + 225 = 0 /\ x >= 15 /**/
<=> (x = 17 + sqrt(289-225) \/ x = 17 - sqrt(289-225) ) /\ x >= 15 /**/
<=> (x = 17 + 8 \/ x = 17 - 8 ) /\ x >= 15 /**/
<=> x = 25