proposition: Lemma rho_t_2 : forall t : TimeT, (rho_V * t < 2)%R.
proof: Proof. Proof with trivial. intro t; apply Rlt_trans with (PI / 2)%R... apply rho_t_PI2... apply Rlt_le_trans with (PI_ub / 2)%R... unfold Rdiv in |- *; repeat rewrite <- (Rmult_comm (/ 2))... apply Rmult_lt_compat_l... apply Rinv_0_lt_compat; prove_sup... assert (H := PI_approx); elim H... right; unfold PI_ub in |- *; unfold Rdiv in |- *. change 4%R with (IZR (2 * 2)). rewrite (mult_IZR 2 2). rewrite Rmult_assoc; rewrite <- Rinv_r_sym; [ apply Rmult_1_r | discrR ]... Qed.
imports: Reals trajectory_const rrho trajectory_def