proposition: Lemma xp0_pos : Omega (beta + thetat intr 0) = true -> (0 <= xp 0)%R.
proof: Proof. Proof with trivial. intro; generalize (Omega_defeq (beta + thetat intr 0) H); intro; rewrite xp0; replace (- l * cos (thetat intr 0 + beta))%R with (l * - cos (thetat intr 0 + beta))%R... apply Rmult_le_pos... apply l_is_pos... rewrite <- neg_cos_var; unfold Rminus in |- *; elim H0; intros; apply cos_ge_0... apply Rplus_le_reg_l with PI; replace (PI + - (PI / 2))%R with (PI / 2)%R... rewrite (Rplus_comm PI); repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; rewrite <- (Rplus_comm beta)... pattern PI at 2 in |- *; rewrite double_var; ring... apply Rplus_le_reg_l with PI; replace (PI + PI / 2)%R with (3 * (PI / 2))%R... rewrite (Rplus_comm PI); repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; rewrite <- (Rplus_comm beta)... pattern PI at 2 in |- *; rewrite double_var; ring... ring... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega