proposition: Lemma Math_prop_alarm_2 : forall (a l : R) (T : TimeT), (MinDistance T <= l)%R -> (l <= MaxDistance T)%R -> (2 * PI - MinBeta <= a)%R -> (a <= 2 * PI)%R -> (Rsqr (l * cos a - v V * T) + Rsqr (l * sin a) <= Rsqr AlertRange)%R.
proof: Proof. intros. cut (0 <= 2 * PI - a)%R. cut (2 * PI - a <= MinBeta)%R. cut (cos (2 * PI - a) = cos a). cut (sin (2 * PI - a) = (- sin a)%R). intros; rewrite Rsqr_mult; rewrite (Rsqr_neg (sin a)); rewrite <- H3; rewrite <- H4; rewrite <- Rsqr_mult; apply (Math_prop_alarm_1 (2 * PI - a) l T H H0 H6 H5). replace (2 * PI - a)%R with (- a + 2 * INR 1 * PI)%R; [ rewrite (sin_period (- a) 1); apply sin_neg | simpl; ring ]. replace (2 * PI - a)%R with (- a + 2 * INR 1 * PI)%R; [ rewrite (cos_period (- a) 1); apply cos_neg | simpl; ring ]. generalize (Rplus_le_compat_l (MinBeta - a) (2 * PI - MinBeta) a H1); replace (MinBeta - a + (2 * PI - MinBeta))%R with (2 * PI - a)%R; [ replace (MinBeta - a + a)%R with MinBeta; [ intro; assumption | ring ] | ring ]. generalize (Rplus_le_compat_r (- a) a (2 * PI) H2); rewrite Rplus_opp_r; intro; assumption. Qed.
imports: Reals trajectory_const rrho constants Omega