proposition: Lemma m_le : forall t1 t2 : TimeT, (t1 <= t2)%R -> (m t1 <= m t2)%R.
proof: Proof. Proof with trivial. intros; unfold m in |- *; repeat rewrite Rmult_assoc... repeat apply Rmult_le_compat_l... left; simpl in |- *; prove_sup... left; apply r_V_is_pos... generalize (rho_t_PI2 t1); intro H1... generalize (rho_t_PI2 t2); intro H2... assert (Hyp : (0 < 2)%R)... prove_sup0... generalize (Rmult_lt_compat_l (/ 2) (rho_V * t1) (PI / 2) (Rinv_0_lt_compat 2 Hyp) H1)... generalize (Rmult_lt_compat_l (/ 2) (rho_V * t2) (PI / 2) (Rinv_0_lt_compat 2 Hyp) H2)... replace (/ 2 * (PI / 2))%R with (PI / 4)%R... clear H1 H2; intros H1 H2... rewrite Rmult_comm in H1... rewrite Rmult_comm in H2... unfold Rdiv in |- *... generalize (cond_1 t1)... generalize (cond_1 t2)... generalize MinT_is_pos; intro H7... intros H3 H4... generalize (Rlt_le_trans 0 MinT t1 H7 H4); clear H4; intro H4... generalize (Rlt_le_trans 0 MinT t2 H7 H3); clear H3; intro H3... apply sin_incr_1... left; apply Rlt_trans with 0%R... apply _PI2_RLT_0... repeat simple apply Rmult_lt_0_compat... apply rho_V_is_pos... apply Rinv_0_lt_compat; simpl in |- *; prove_sup0... left; apply Rlt_trans with (PI / 4)%R... rewrite <- Rmult_assoc... apply PI4_RLT_PI2... left; apply Rlt_trans with 0%R... apply _PI2_RLT_0... repeat simple apply Rmult_lt_0_compat... apply rho_V_is_pos... apply Rinv_0_lt_compat; simpl in |- *; prove_sup0... left; apply Rlt_trans with (PI / 4)%R... rewrite <- Rmult_assoc... apply PI4_RLT_PI2... apply Rmult_le_compat_l... left; apply rho_V_is_pos... apply Rmult_le_compat_r... left; apply Rinv_0_lt_compat; simpl in |- *; prove_sup0... unfold Rdiv in |- *; rewrite (Rmult_comm (/ 2)); rewrite Rmult_assoc; rewrite <- Rinv_mult_distr... Qed.
imports: Reals trajectory_const rrho trajectory_def