proposition: Lemma tmin_0 : forall intruder evader : State, div_tau intruder evader <> 0%R -> tmin intruder evader = (- Bx_R intruder evader / (2 * Ax2_R intruder))%R.
proof: Proof. intros; unfold tmin in |- *; case (Req_EM_var (div_tau intruder evader) 0); intro. elim H; assumption. unfold div_tau, Bx_R, Ax2_R in |- *; unfold dxdt, dydt in |- *; unfold Rdiv in |- *; rewrite Rinv_mult_distr. replace (Rsqr (sind (heading intruder) * intruderSpeed) + Rsqr (- evaderSpeed + cosd (heading intruder) * intruderSpeed))%R with (Rsqr (intruderSpeed * cosd (heading intruder) - evaderSpeed) + Rsqr (intruderSpeed * sind (heading intruder)))%R. apply Rmult_eq_reg_l with (Rsqr (intruderSpeed * cosd (heading intruder) - evaderSpeed) + Rsqr (intruderSpeed * sind (heading intruder)))%R. rewrite (Rmult_comm (Rsqr (intruderSpeed * cosd (heading intruder) - evaderSpeed) + Rsqr (intruderSpeed * sind (heading intruder)))) ; repeat rewrite Rmult_assoc; rewrite <- (Rinv_l_sym (Rsqr (intruderSpeed * cosd (heading intruder) - evaderSpeed) + Rsqr (intruderSpeed * sind (heading intruder)))) . rewrite Rmult_1_r; rewrite (Rmult_comm (Rsqr (intruderSpeed * cosd (heading intruder) - evaderSpeed) + Rsqr (intruderSpeed * sind (heading intruder)))) ; repeat rewrite Rmult_assoc; rewrite <- (Rinv_l_sym (Rsqr (intruderSpeed * cosd (heading intruder) - evaderSpeed) + Rsqr (intruderSpeed * sind (heading intruder)))) . rewrite Rmult_1_r; replace (- (-2 * (yt evader * (sind (heading intruder) * intruderSpeed)) + 2 * (yt intruder * (sind (heading intruder) * intruderSpeed)) - 2 * (cosd (heading intruder) * (xt evader * intruderSpeed)) + 2 * (cosd (heading intruder) * (xt intruder * intruderSpeed)) + 2 * (xt evader * evaderSpeed) - 2 * (xt intruder * evaderSpeed)))%R with ((yt evader * (sind (heading intruder) * intruderSpeed) - yt intruder * (sind (heading intruder) * intruderSpeed) + cosd (heading intruder) * (xt evader * intruderSpeed) - cosd (heading intruder) * (xt intruder * intruderSpeed) - xt evader * evaderSpeed + xt intruder * evaderSpeed) * 2)%R. repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym. rewrite Rmult_1_r; ring. discrR. ring. unfold div_tau in H; unfold dxdt, dydt in H; assumption. assumption. assumption. cut ((intruderSpeed * cosd (heading intruder) - evaderSpeed)%R = (- evaderSpeed + cosd (heading intruder) * intruderSpeed)%R). cut ((intruderSpeed * sind (heading intruder))%R = (sind (heading intruder) * intruderSpeed)%R). intros; rewrite H0; rewrite H1; rewrite Rplus_comm; reflexivity. ring. ring. discrR. cut ((intruderSpeed * cosd (heading intruder) - evaderSpeed)%R = (- evaderSpeed + cosd (heading intruder) * intruderSpeed)%R). cut ((intruderSpeed * sind (heading intruder))%R = (sind (heading intruder) * intruderSpeed)%R). intros; rewrite <- H0; rewrite <- H1; rewrite Rplus_comm; assumption. ring. ring. Qed.
imports: Reals ails_def trajectory_const