proposition: Lemma Math_prop_y_a_PI2 : forall (a l : R) (T : TimeT), (MinBeta <= a)%R -> (a <= PI / 2)%R -> (0 <= l)%R -> (l * sin MinBeta + r_V * (cos (rho_V * T) - 1) <= l * sin a + r_V * (cos (rho_V * T) - 1))%R.
proof: Proof. intros; apply Rplus_le_compat_r; apply Rmult_le_compat_l; [ assumption | apply sin_incr_1; [ left; apply Rlt_trans with 0%R; [ apply _PI2_RLT_0 | apply MinBeta_pos ] | apply Rle_trans with a; assumption | left; apply Rlt_trans with 0%R; [ apply _PI2_RLT_0 | apply Rlt_le_trans with MinBeta; [ apply MinBeta_pos | assumption ] ] | assumption | assumption ] ]. Qed.
imports: Reals trajectory_const rrho constants Omega