proposition: Lemma R_equal_when_zero : forall (intruder evader : State) (t1 t2 : R), div_tau intruder evader = 0%R -> RR intruder evader t1 = RR intruder evader t2.
proof: Proof. intros; unfold RR in |- *; unfold div_tau in H; generalize (Rplus_eq_R0 (Rsqr (dxdt intruder)) (Rsqr (dydt intruder)) (Rle_0_sqr (dxdt intruder)) (Rle_0_sqr (dydt intruder)) H); intro; elim H0; intros; generalize (Rsqr_eq_0 (dxdt intruder) H1); intro; generalize (Rsqr_eq_0 (dydt intruder) H2); intro; rewrite <- (dx_dxdt intruder evader t1); rewrite <- (dx_dxdt intruder evader t2); rewrite <- (dy_dydt intruder evader t1); rewrite <- (dy_dydt intruder evader t2); rewrite H3; rewrite H4; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; reflexivity. Qed.
imports: Reals ails_def trajectory_const