proposition: Theorem rho_ub_t_PI2 : forall (h : TypeSpeed) (t : TimeT), (rho_ub h * t < PI / 2)%R.
proof: Proof. Proof with trivial. intros; assert (H := cond_2 t)... unfold MaxT in H; apply Rlt_trans with (PI_lb / 2)%R... unfold rho_ub in |- *; cut (g < 33)%R... cut (tan_ub_MaxBank < 4 / 5)%R... cut (/ h < / 200)%R... intros; generalize g_pos; intro H3; generalize tan_ub_MaxBank_pos; intro H4; generalize (Rinv_0_lt_compat h (TypeSpeed_pos h)); intro H5... generalize (Rmult_le_0_lt_compat g 33 tan_ub_MaxBank (4 / 5) (Rlt_le 0 g H3) (Rlt_le 0 tan_ub_MaxBank H4) H2 H1)... intro H6; generalize (Rmult_lt_0_compat g tan_ub_MaxBank H3 H4); intro H7... assert (H8 := Rmult_le_0_lt_compat (g * tan_ub_MaxBank) (33 * (4 / 5)) (/ h) (/ 200) (Rlt_le 0 (g * tan_ub_MaxBank) H7) (Rlt_le 0 (/ h) H5) H6 H0)... apply Rlt_trans with (33 * / 200 * (4 / 5) * t)%R... apply Rmult_lt_compat_r... apply Rlt_le_trans with MinT... apply MinT_is_pos... apply (cond_1 t)... rewrite Rmult_assoc; rewrite (Rmult_comm (/ 200)); unfold Rdiv in |- *; do 2 rewrite <- Rmult_assoc... apply Rle_lt_trans with (33 * / 200 * (4 / 5) * 10)%R... apply Rmult_le_compat_l... left; apply Rmult_lt_0_compat... apply Rmult_lt_0_compat; [ prove_sup | apply Rinv_0_lt_compat; prove_sup ]... unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ prove_sup | apply Rinv_0_lt_compat; prove_sup ]... apply Rmult_lt_reg_l with 2%R... prove_sup... apply Rmult_lt_reg_l with 200%R... prove_sup... apply Rmult_lt_reg_l with 5%R... prove_sup... set (x := 200%R); set (y := 33%R); set (z := 10%R); set (u := 5%R); set (v := 4%R); set (w := 2%R)... unfold Rdiv in |- *; replace (u * (x * (w * (PI_lb * / w))))%R with (x * PI_lb * u * (w * / w))%R; [ idtac | ring ]... replace (u * (x * (w * (y * / x * (v * / u) * z))))%R with (w * y * v * z * (u * / u) * (x * / x))%R; [ idtac | ring ]... repeat rewrite <- Rinv_r_sym; unfold x, y, z, u, v, w in |- *; try discrR... unfold PI_lb in |- *; prove_sup... apply Rinv_lt_contravar... apply Rmult_lt_0_compat... prove_sup... apply Rlt_le_trans with MinSpeed... unfold MinSpeed in |- *; prove_sup... apply (v_cond1 h)... apply Rlt_le_trans with MinSpeed... unfold MinSpeed in |- *; prove_sup... apply (v_cond1 h)... unfold tan_ub_MaxBank in |- *; unfold Rdiv in |- *... apply Rmult_lt_reg_l with 10%R... prove_sup... rewrite (Rmult_comm 10); rewrite Rmult_assoc; rewrite <- Rinv_l_sym... rewrite Rmult_1_r; apply Rmult_lt_reg_l with 5%R... prove_sup... pattern 5%R at 1 in |- *; rewrite (Rmult_comm 5); do 2 rewrite Rmult_assoc; rewrite <- Rinv_l_sym... prove_sup... discrR... discrR... unfold g in |- *; unfold Rdiv in |- *; apply Rmult_lt_reg_l with 10%R... prove_sup... rewrite <- Rmult_comm; rewrite Rmult_assoc; rewrite <- Rinv_l_sym... rewrite Rmult_1_r; prove_sup... discrR... unfold Rdiv in |- *; repeat rewrite <- (Rmult_comm (/ 2)); apply Rmult_lt_compat_l... apply Rinv_0_lt_compat; prove_sup... assert (H0 := PI_approx); elim H0... Qed.
imports: Reals trajectory_const rrho trajectory_def