proposition: Lemma G_0 : G 0 = 0%R.
proof: Proof. unfold G in |- *; rewrite Rs_0; unfold Rminus, F in |- *; unfold Rdiv in |- *; rewrite Rmult_0_l; rewrite Rmult_0_r; rewrite sin_0; repeat rewrite Rmult_0_r; rewrite Rplus_0_l; apply Ropp_0. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho