proposition: Lemma no_conflict_xp_1_Omega : forall t : R, (1 <= t)%R -> (rho_vi * t <= PI - rho_vi)%R -> Omega (beta + thetat intr 0) = true -> (ConflictRange < xp t)%R.
proof: Proof. Proof with trivial. intros; apply Rlt_le_trans with (r_vi * sin rho_vi)%R... apply r_sin_rho... apply Rle_trans with (r_vi * sin (rho_vi * t))%R... apply Rmult_le_compat_l... left; unfold r_vi in |- *; unfold r in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat... apply TypeSpeed_pos... apply Rinv_0_lt_compat; apply rho_pos... case (Rle_dec (rho_vi * t) (PI / 2)); intro... cut (rho_vi <= rho_vi * t)%R... intro; apply sin_incr_1... left; apply Rlt_trans with 0%R... apply _PI2_RLT_0... unfold rho_vi in |- *; apply rho_pos... apply Rle_trans with (rho_vi * t)%R... left; apply Rlt_le_trans with 0%R... apply _PI2_RLT_0... apply rho_t_pos... left; apply Rlt_le_trans with 1%R; try apply Rlt_0_1... pattern rho_vi at 1 in |- *; rewrite <- (Rmult_1_r rho_vi)... apply Rmult_le_compat_l... left; unfold rho_vi in |- *; apply rho_pos... cut (PI / 2 < rho_vi * t)%R... intro; cut (rho_vi <= PI - rho_vi * t)%R... cut (PI - rho_vi * t <= PI / 2)%R... intros; rewrite <- (sin_PI_x (rho_vi * t))... apply sin_incr_1... left; apply Rlt_trans with 0%R... apply _PI2_RLT_0... unfold rho_vi in |- *; apply rho_pos... apply Rle_trans with (PI - rho_vi * t)%R... apply Rle_trans with rho_vi... left; apply Rlt_trans with 0%R... apply _PI2_RLT_0... unfold rho_vi in |- *; apply rho_pos... left... apply Rplus_lt_reg_l with (- (PI / 2) + rho_vi * t)%R... replace (- (PI / 2) + rho_vi * t + (PI - rho_vi * t))%R with (PI / 2)%R... replace (- (PI / 2) + rho_vi * t + PI / 2)%R with (rho_vi * t)%R... ring... unfold Rminus in |- *; unfold Rdiv in |- *; replace (- (PI * / 2) + rho_vi * t + (PI + - (rho_vi * t)))%R with (- (PI * / 2) + PI + (rho_vi * t + - (rho_vi * t)))%R... rewrite Rplus_opp_r; rewrite Rplus_0_r... pattern PI at 3 in |- *; rewrite double_var... unfold Rdiv in |- *; ring... ring... apply Rplus_le_reg_l with (rho_vi * t - rho_vi)%R... unfold Rminus in |- *... repeat rewrite Rplus_assoc... rewrite Rplus_opp_l; rewrite Rplus_0_r... rewrite (Rplus_comm (rho_vi * t))... repeat rewrite Rplus_assoc... rewrite Rplus_opp_l; rewrite Rplus_0_r... rewrite <- (Rplus_comm PI)... auto with real... cut (0 <= t)%R... cut (rho_vi * t <= PI)%R... intros... generalize (xpt t H3 H2); intro... generalize (xp0_pos H1); intro... unfold Rminus in H4... generalize (Rplus_le_compat_r (xp 0) (hx t) (xp t + - xp 0) H4)... repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r... intro... generalize (plus_le_is_le (hx t) (xp 0) (xp t) H5 H6)... apply Rle_trans with (PI - rho_vi)%R... apply Rplus_le_reg_l with (- PI)%R... unfold Rminus in |- *... repeat rewrite <- Rplus_assoc... repeat rewrite Rplus_opp_l... rewrite Rplus_0_l... rewrite <- Ropp_0... apply Ropp_ge_le_contravar; apply Rle_ge; left; unfold rho_vi in |- *; apply rho_pos... left; apply Rlt_le_trans with 1%R; try apply Rlt_0_1... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega