proposition: Lemma alphas_def : forall t : R, xi intr t = (Rs t * cos (alphas t) + xi intr 0)%R /\ yi intr t = (Rs t * sin (alphas t) + yi intr 0)%R.
proof: Proof. unfold alphas in |- *; case alphas_exists; trivial. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho