proposition: Lemma R_Rmin : forall (intruder evader : State) (t : R), div_tau intruder evader <> 0%R -> Rsqr (RR intruder evader t) = (Ax2_R intruder * Rsqr (t - tmin intruder evader) + Rsqr_Rmin intruder evader)%R.
proof: Proof. Proof with trivial. intros; unfold Rsqr_Rmin in |- *; case (Req_EM_var (Ax2_R intruder) 0); intro... elim H; apply div_tau_0_Ax2_R... rewrite Rsqr_minus; rewrite (tmin_0 intruder evader H); rewrite Rsqr_div... unfold Rdiv in |- *; rewrite Rsqr_R; rewrite <- Rsqr_neg; rewrite Rsqr_mult; replace (Rsqr 2) with 4%R... rewrite (Rinv_mult_distr 2 (Ax2_R intruder))... rewrite (Rinv_mult_distr 4 (Ax2_R intruder))... rewrite Rinv_mult_distr... unfold Rminus in |- *; do 2 rewrite Rmult_plus_distr_l... rewrite <- (Rmult_comm (Rsqr (Bx_R intruder evader) * (/ 4 * / Rsqr (Ax2_R intruder)))) ; unfold Rsqr in |- *; rewrite (Rinv_mult_distr (Ax2_R intruder) (Ax2_R intruder))... repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... rewrite Rmult_1_r... repeat rewrite Rplus_assoc; apply Rplus_eq_compat_l... rewrite (Rmult_plus_distr_r (4 * (Ax2_R intruder * C_R intruder evader)) (- (Bx_R intruder evader * Bx_R intruder evader)) (/ 4 * / Ax2_R intruder))... replace (Ax2_R intruder * - (2 * (t * (- Bx_R intruder evader * (/ 2 * / Ax2_R intruder)))))%R with (Bx_R intruder evader * t)%R... replace (4 * (Ax2_R intruder * C_R intruder evader) * (/ 4 * / Ax2_R intruder))%R with (C_R intruder evader)... ring... rewrite (Rmult_comm (/ 4))... repeat rewrite Rmult_assoc... rewrite (Rmult_comm 4)... repeat rewrite Rmult_assoc... rewrite <- Rinv_l_sym... rewrite Rmult_1_r; rewrite (Rmult_comm (C_R intruder evader)); repeat rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym... symmetry in |- *; apply Rmult_1_l... discrR... rewrite (Rmult_comm (Ax2_R intruder)); replace (- (2 * (t * (- Bx_R intruder evader * (/ 2 * / Ax2_R intruder)))))%R with (-2 * t * - Bx_R intruder evader * / 2 * / Ax2_R intruder)%R... repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... rewrite Rmult_1_r; repeat rewrite <- Rmult_assoc; replace (-2 * t * - Bx_R intruder evader)%R with (t * Bx_R intruder evader * 2)%R... repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym... ring... discrR... ring... ring... discrR... unfold Rsqr in |- *; apply prod_neq_R0... discrR... discrR... apply prod_neq_R0... Qed.
imports: Reals ails_def trajectory_const