proposition: Lemma Rsqr_R : forall (intruder evader : State) (t : R), Rsqr (RR intruder evader t) = (Ax2_R intruder * Rsqr t + Bx_R intruder evader * t + C_R intruder evader)%R.
proof: Proof. intros; unfold RR in |- *; unfold dx, dy in |- *; rewrite Rsqr_sqrt; [ replace (xt intruder + t * intruderSpeed * cosd (heading intruder) - (xt evader + t * evaderSpeed))%R with ((- evaderSpeed + cosd (heading intruder) * intruderSpeed) * t + (xt intruder - xt evader))%R; [ replace (yt intruder + t * intruderSpeed * sind (heading intruder) - yt evader)%R with (sind (heading intruder) * intruderSpeed * t + (yt intruder - yt evader))%R; [ repeat rewrite Rsqr_plus; repeat rewrite Rsqr_mult; unfold Ax2_R in |- *; apply Rplus_eq_reg_l with (- (Rsqr (sind (heading intruder) * intruderSpeed) + Rsqr (- evaderSpeed + cosd (heading intruder) * intruderSpeed)) * Rsqr t)%R; replace (- (Rsqr (sind (heading intruder) * intruderSpeed) + Rsqr (- evaderSpeed + cosd (heading intruder) * intruderSpeed)) * Rsqr t + (Rsqr (- evaderSpeed + cosd (heading intruder) * intruderSpeed) * Rsqr t + Rsqr (xt intruder - xt evader) + 2 * ((- evaderSpeed + cosd (heading intruder) * intruderSpeed) * t) * (xt intruder - xt evader) + (Rsqr (sind (heading intruder)) * Rsqr intruderSpeed * Rsqr t + Rsqr (yt intruder - yt evader) + 2 * (sind (heading intruder) * intruderSpeed * t) * (yt intruder - yt evader))))%R with (Rsqr (xt intruder - xt evader) + 2 * ((- evaderSpeed + cosd (heading intruder) * intruderSpeed) * t) * (xt intruder - xt evader) + Rsqr (yt intruder - yt evader) + 2 * (sind (heading intruder) * intruderSpeed * t) * (yt intruder - yt evader))%R; [ replace (- (Rsqr (sind (heading intruder) * intruderSpeed) + Rsqr (- evaderSpeed + cosd (heading intruder) * intruderSpeed)) * Rsqr t + ((Rsqr (sind (heading intruder) * intruderSpeed) + Rsqr (- evaderSpeed + cosd (heading intruder) * intruderSpeed)) * Rsqr t + Bx_R intruder evader * t + C_R intruder evader))%R with (Bx_R intruder evader * t + C_R intruder evader)%R; [ unfold C_R in |- *; apply Rplus_eq_reg_l with (- (Rsqr (yt intruder - yt evader) + Rsqr (xt intruder - xt evader)))%R; replace (- (Rsqr (yt intruder - yt evader) + Rsqr (xt intruder - xt evader)) + (Rsqr (xt intruder - xt evader) + 2 * ((- evaderSpeed + cosd (heading intruder) * intruderSpeed) * t) * (xt intruder - xt evader) + Rsqr (yt intruder - yt evader) + 2 * (sind (heading intruder) * intruderSpeed * t) * (yt intruder - yt evader)))%R with (2 * ((- evaderSpeed + cosd (heading intruder) * intruderSpeed) * t) * (xt intruder - xt evader) + 2 * (sind (heading intruder) * intruderSpeed * t) * (yt intruder - yt evader))%R; [ replace (- (Rsqr (yt intruder - yt evader) + Rsqr (xt intruder - xt evader)) + (Bx_R intruder evader * t + (Rsqr (yt intruder - yt evader) + Rsqr (xt intruder - xt evader))))%R with (Bx_R intruder evader * t)%R; [ unfold Bx_R in |- *; ring | ring ] | ring ] | ring ] | rewrite (Rsqr_mult (sind (heading intruder)) intruderSpeed); ring ] | ring ] | ring ] | apply Rplus_le_le_0_compat; apply Rle_0_sqr ]. Qed.
imports: Reals ails_def trajectory_const