if x < -0.23566085f0

1. Started with
   \[\frac{1 - \cos x}{{x}^2}\]
   1.1
2. Using strategy rm
   1.1
3. Applied square-mult to get
   \[\frac{1 - \cos x}{\color{red}{{x}^2}} \leadsto \frac{1 - \cos x}{\color{blue}{x \cdot x}}\]
   1.1
4. Applied *-un-lft-identity to get
   \[\frac{\color{red}{1 - \cos x}}{x \cdot x} \leadsto \frac{\color{blue}{1 \cdot \left(1 - \cos x\right)}}{x \cdot x}\]
   1.1
5. Applied times-frac to get
   \[\color{red}{\frac{1 \cdot \left(1 - \cos x\right)}{x \cdot x}} \leadsto \color{blue}{\frac{1}{x} \cdot \frac{1 - \cos x}{x}}\]
   0.4

if -0.23566085f0 < x < 0.5589793f0

1. Started with
   \[\frac{1 - \cos x}{{x}^2}\]
   28.5
2. Applied taylor to get
   \[\frac{1 - \cos x}{{x}^2} \leadsto \left(\frac{1}{720} \cdot {x}^{4} + \frac{1}{2}\right) - \frac{1}{24} \cdot {x}^2\]
   0
3. Taylor expanded around 0 to get
   \[\color{red}{\left(\frac{1}{720} \cdot {x}^{4} + \frac{1}{2}\right) - \frac{1}{24} \cdot {x}^2} \leadsto \color{blue}{\left(\frac{1}{720} \cdot {x}^{4} + \frac{1}{2}\right) - \frac{1}{24} \cdot {x}^2}\]
   0

if 0.5589793f0 < x

1. Started with
   \[\frac{1 - \cos x}{{x}^2}\]
   1.2
2. Using strategy rm
   1.2
3. Applied flip-- to get
   \[\frac{\color{red}{1 - \cos x}}{{x}^2} \leadsto \frac{\color{blue}{\frac{{1}^2 - {\left(\cos x\right)}^2}{1 + \cos x}}}{{x}^2}\]
   1.2
4. Applied simplify to get
   \[\frac{\frac{\color{red}{{1}^2 - {\left(\cos x\right)}^2}}{1 + \cos x}}{{x}^2} \leadsto \frac{\frac{\color{blue}{{\left(\sin x\right)}^2}}{1 + \cos x}}{{x}^2}\]
   1.3
5. Using strategy rm
   1.3
6. Applied add-sqr-sqrt to get
   \[\frac{\color{red}{\frac{{\left(\sin x\right)}^2}{1 + \cos x}}}{{x}^2} \leadsto \frac{\color{blue}{{\left(\sqrt{\frac{{\left(\sin x\right)}^2}{1 + \cos x}}\right)}^2}}{{x}^2}\]
   1.4
7. Applied square-undiv to get
   \[\color{red}{\frac{{\left(\sqrt{\frac{{\left(\sin x\right)}^2}{1 + \cos x}}\right)}^2}{{x}^2}} \leadsto \color{blue}{{\left(\frac{\sqrt{\frac{{\left(\sin x\right)}^2}{1 + \cos x}}}{x}\right)}^2}\]
   0.5