proposition: Lemma xp0 : xp 0 = (- l * cos (thetat intr 0 + beta))%R.
proof: Proof. unfold xp in |- *; rewrite xe_0; rewrite ye_0; rewrite <- (Rplus_comm (xi intr 0)); unfold Rminus in |- *; repeat rewrite Ropp_plus_distr; repeat rewrite <- Rplus_assoc; repeat rewrite Rplus_opp_r; repeat rewrite Rplus_0_l; rewrite cos_plus; ring. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega