proposition: Lemma tau_tmin : forall (intruder evader : State) (t : R), div_tau intruder evader <> 0%R -> tau intruder evader t = (tmin intruder evader - t)%R.
proof: Proof. intros. cut (tau intruder evader t = (- (dx intruder evader t * dxdt intruder + dy intruder evader t * dydt intruder) / div_tau intruder evader)%R). cut (tmin intruder evader = (- (dxdt intruder * (xt intruder - xt evader) + dydt intruder * (yt intruder - yt evader)) / div_tau intruder evader)%R). intros. rewrite H0; rewrite H1. unfold Rdiv in |- *. replace (- (dxdt intruder * (xt intruder - xt evader) + dydt intruder * (yt intruder - yt evader)) * / div_tau intruder evader - t)%R with (- (dxdt intruder * (xt intruder - xt evader + t * dxdt intruder) + dydt intruder * (yt intruder - yt evader + t * dydt intruder)) / div_tau intruder evader)%R. cut ((xt intruder - xt evader + t * dxdt intruder)%R = dx intruder evader t). cut ((yt intruder - yt evader + t * dydt intruder)%R = dy intruder evader t). intros; rewrite H2; rewrite H3; unfold Rdiv in |- *; rewrite (Rmult_comm (dx intruder evader t)); rewrite (Rmult_comm (dy intruder evader t)); reflexivity. unfold dydt, dy in |- *; ring. unfold dxdt, dx in |- *; ring. unfold Rdiv in |- *; apply (Rmult_eq_reg_l (div_tau intruder evader)). rewrite (Rmult_comm (div_tau intruder evader)); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. rewrite Rmult_1_r; rewrite (Rmult_comm (div_tau intruder evader)); replace ((- (dxdt intruder * (xt intruder - xt evader) + dydt intruder * (yt intruder - yt evader)) * / div_tau intruder evader - t) * div_tau intruder evader)%R with (- (dxdt intruder * (xt intruder - xt evader) + dydt intruder * (yt intruder - yt evader)) * / div_tau intruder evader * div_tau intruder evader - t * div_tau intruder evader)%R. repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. rewrite Rmult_1_r; unfold div_tau in |- *; unfold Rsqr in |- *; ring. assumption. symmetry in |- *; unfold Rminus in |- *; replace (- (dxdt intruder * (xt intruder + - xt evader) + dydt intruder * (yt intruder + - yt evader)) * / div_tau intruder evader + - t)%R with (- (dxdt intruder * (xt intruder + - xt evader) + dydt intruder * (yt intruder + - yt evader)) * / div_tau intruder evader + - t)%R. replace (- (t * div_tau intruder evader))%R with (- t * div_tau intruder evader)%R. replace (- (dxdt intruder * (xt intruder + - xt evader) + dydt intruder * (yt intruder + - yt evader)) * / div_tau intruder evader * div_tau intruder evader)%R with (- (dxdt intruder * (xt intruder + - xt evader) + dydt intruder * (yt intruder + - yt evader)) * / div_tau intruder evader * div_tau intruder evader)%R. apply Rmult_plus_distr_r. ring. ring. ring. assumption. assumption. unfold tmin in |- *; case (Req_EM_var (div_tau intruder evader) 0); intro. rewrite e in H; elim H; reflexivity. reflexivity. unfold tau in |- *; case (Req_EM_var (div_tau intruder evader) 0); intro. rewrite e in H; elim H; reflexivity. reflexivity. Qed.
imports: Reals ails_def trajectory_const