proposition: Lemma Rsx : forall t : R, xi intr t = (xi intr 0 + Rs t * cos (alphas t))%R.
proof: Proof. intros; generalize (alphas_def t); intro H; elim H; intros; rewrite Rplus_comm; assumption. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho