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