proposition: Lemma Rs_y : forall t : R, sin (alphas t) <> 0%R -> Rs t = ((yi intr t - yi intr 0) / sin (alphas t))%R.
proof: Proof. intros; rewrite Rsy; unfold Rminus, Rdiv in |- *; rewrite (Rplus_comm (yi intr 0)); rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r; rewrite Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_r; reflexivity | assumption ]. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho