In this video we demonstrate how to use the differential auxiliaries proof rule in KeYmaera. Differential auxiliaries, sometimes referred to as differential ghosts, are useful when we have a differential equation which is not solvable in real arithmetic, or which is computationally intractable. In a previous video, we looked at differential invariants for dealing with these tricky differential equations, and in fact, differential invariants and differential auxiliaries go hand-in-hand. In some cases there is not a strong enough differential invariant to prove the property given the variables available in the system. In these cases we can rewrite the property we want to prove using an auxiliary variable, and then allow the auxiliary variable to evolve in a way that we choose.