proposition: Lemma div_tau_0_Ax2_R : forall intruder evader : State, Ax2_R intruder = 0%R -> div_tau intruder evader = 0%R.
proof: Proof. unfold div_tau, Ax2_R in |- *; intros; unfold dxdt, dydt in |- *; replace (intruderSpeed * cosd (heading intruder) - evaderSpeed)%R with (- evaderSpeed + cosd (heading intruder) * intruderSpeed)%R; [ rewrite <- (Rmult_comm (sind (heading intruder))); rewrite Rplus_comm; assumption | ring ]. Qed.
imports: Reals ails_def trajectory_const