proposition: Lemma Math_prop_no_conflict_2 : forall (a l x y : R) (T : TimeT), (MinDistance T <= l)%R -> (l <= MaxDistance T)%R -> (3 * (PI / 2) <= a)%R -> (a <= 2 * PI - MinBeta)%R -> (y <= l * sin a - r_V * (cos (rho_V * T) - 1))%R -> (r_V * sin (rho_V * T) - l * cos a <= x)%R -> (Rsqr ConflictRange < Rsqr x + Rsqr y)%R.
proof: Proof. intros. cut (MinBeta <= 2 * PI - a)%R. cut (2 * PI - a <= PI / 2)%R. cut (l * sin (2 * PI - a) + r_V * (cos (rho_V * T) - 1) <= - y)%R. intros; rewrite (Rsqr_neg y); apply (Math_prop_no_conflict_1 (2 * PI - a) l x (- y) T H H0 H7 H6 H5). replace (2 * PI - a)%R with (- a + 2 * INR 1 * PI)%R; [ rewrite (cos_period (- a) 1); rewrite cos_neg; assumption | simpl; ring ]. replace (2 * PI - a)%R with (- a + 2 * INR 1 * PI)%R; [ rewrite (sin_period (- a) 1); rewrite sin_neg; replace (l * - sin a + r_V * (cos (rho_V * T) - 1))%R with (- (l * sin a - r_V * (cos (rho_V * T) - 1)))%R; [ apply Ropp_ge_le_contravar; apply Rle_ge; assumption | simpl; ring ] | simpl; ring ]. generalize (Rplus_le_compat_l (PI / 2 - a) (3 * (PI / 2)) a H1); replace (PI / 2 - a + 3 * (PI / 2))%R with (2 * PI - a)%R. replace (PI / 2 - a + a)%R with (PI / 2)%R. intro; assumption. unfold Rminus in |- *; rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; reflexivity. rewrite double. pattern PI at 1 2 in |- *; rewrite double_var. ring. generalize (Rplus_le_compat_l (MinBeta - a) a (2 * PI - MinBeta) H2); replace (MinBeta - a + (2 * PI - MinBeta))%R with (2 * PI - a)%R; [ replace (MinBeta - a + a)%R with MinBeta; [ intro; assumption | ring ] | ring ]. Qed.
imports: Reals trajectory_const rrho constants Omega