proposition: Theorem rho_t_PI2 : forall t : TimeT, (rho_V * t < PI / 2)%R.
proof: Proof. Proof with trivial. intro; generalize (rho_ub_t_PI2 V t); intro; unfold rho_V in |- *... apply Rlt_trans with (rho_ub V * t)%R... apply Rmult_lt_compat_r... apply Rlt_le_trans with MinT; [ apply MinT_is_pos | apply (cond_1 t) ]... apply rho_ub_0... Qed.
imports: Reals trajectory_const rrho trajectory_def