proposition: Lemma rho_PI2 : forall h : TypeSpeed, (rho h <= PI / 2)%R.
proof: Proof. intro h; unfold rho in |- *; unfold Rdiv in |- *. cut (g < 33)%R. cut (tan MaxBank < 1)%R. cut (/ h < / 200)%R. intros; generalize g_pos; intro H2; generalize tan_MaxBank_pos; intro H3; generalize (Rinv_0_lt_compat h (TypeSpeed_pos h)); intro H4. generalize (Rmult_le_0_lt_compat g 33 (tan MaxBank) 1 (Rlt_le 0 g H2) (Rlt_le 0 (tan MaxBank) H3) H1 H0); intro H5; generalize (Rmult_lt_0_compat g (tan MaxBank) H2 H3); intro H6. rewrite Rmult_1_r in H5. generalize (Rmult_le_0_lt_compat (g * tan MaxBank) 33 (/ h) (/ 200) (Rlt_le 0 (g * tan MaxBank) H6) (Rlt_le 0 (/ h) H4) H5 H). intro H7; left. apply Rlt_trans with (33 / 200)%R. unfold Rdiv in |- *; rewrite <- Rmult_assoc; assumption. apply Rlt_le_trans with (PI_lb / 2)%R. apply Rlt_trans with 1%R. unfold Rdiv in |- *; apply Rmult_lt_reg_l with 200%R. prove_sup. rewrite Rmult_1_r; rewrite <- Rmult_comm; rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ prove_sup | discrR ]. apply Rmult_lt_reg_l with 2%R. prove_sup. unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym. rewrite Rmult_1_r; rewrite Rmult_1_l; unfold PI_lb in |- *. prove_sup. discrR. unfold Rdiv in |- *; left; repeat rewrite <- (Rmult_comm (/ 2)); apply Rmult_lt_compat_l. apply Rinv_0_lt_compat; prove_sup. elim PI_approx; intros; assumption. apply Rinv_lt_contravar. apply Rmult_lt_0_compat. prove_sup. apply TypeSpeed_pos. apply Rlt_le_trans with MinSpeed. unfold MinSpeed in |- *; prove_sup. apply (v_cond1 h). apply Rlt_trans with tan_ub_MaxBank. apply tan_MaxBank_ub. unfold tan_ub_MaxBank in |- *; unfold Rdiv in |- *; apply Rmult_lt_reg_l with 10%R. prove_sup. rewrite <- Rmult_comm; rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ prove_sup | 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; [ prove_sup | discrR ]. Qed.
imports: Reals trajectory_const