proposition: Lemma m_rho_T_pos : forall t : TimeT, (0 < m t)%R.
proof: Proof. Proof with trivial. intro t; unfold m in |- *; repeat simple apply Rmult_lt_0_compat... simpl in |- *; prove_sup0... apply r_V_is_pos... generalize (cond_1 t); generalize MinT_is_pos; intros H H0; generalize (Rlt_le_trans 0 MinT t H H0); clear H; intro H; apply sin_gt_0... repeat simple apply Rmult_lt_0_compat... apply rho_V_is_pos... unfold Rdiv in |- *; apply Rmult_lt_0_compat; try (apply Rinv_0_lt_compat; simpl in |- *; prove_sup0)... generalize (rho_t_PI2 t); intro H1; assert (Hyp : (0 < 2)%R)... prove_sup0... generalize (Rmult_lt_compat_r (/ 2) (rho_V * t) (PI / 2) (Rinv_0_lt_compat 2 Hyp) H1); rewrite Rmult_assoc; replace (PI / 2 * / 2)%R with (PI / 4)%R... intro H2; apply Rlt_trans with (PI / 4)%R... apply (Rlt_trans (PI / 4) (PI / 2) PI PI4_RLT_PI2 PI2_Rlt_PI)... unfold Rdiv in |- *; rewrite Rmult_assoc; rewrite <- Rinv_mult_distr... Qed.
imports: Reals trajectory_const rrho trajectory_def