proposition: Lemma neg_cos_var : forall x : R, cos (x - PI) = (- cos x)%R.
proof: Proof. intro; rewrite cos_minus; rewrite cos_PI; rewrite sin_PI; ring. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega