Initial program 0.3
\[\frac{1 - \tan x \cdot \tan x}{1 + \tan x \cdot \tan x}\]
- Using strategy
rm Applied div-sub0.4
\[\leadsto \color{blue}{\frac{1}{1 + \tan x \cdot \tan x} - \frac{\tan x \cdot \tan x}{1 + \tan x \cdot \tan x}}\]
- Using strategy
rm Applied tan-quot0.4
\[\leadsto \frac{1}{1 + \tan x \cdot \color{blue}{\frac{\sin x}{\cos x}}} - \frac{\tan x \cdot \tan x}{1 + \tan x \cdot \tan x}\]
Applied tan-quot0.4
\[\leadsto \frac{1}{1 + \color{blue}{\frac{\sin x}{\cos x}} \cdot \frac{\sin x}{\cos x}} - \frac{\tan x \cdot \tan x}{1 + \tan x \cdot \tan x}\]
Applied frac-times0.4
\[\leadsto \frac{1}{1 + \color{blue}{\frac{\sin x \cdot \sin x}{\cos x \cdot \cos x}}} - \frac{\tan x \cdot \tan x}{1 + \tan x \cdot \tan x}\]