proposition: Lemma ye_0 : ye = (yi intr 0 - l * sin beta)%R.
proof: Proof. Proof with trivial. generalize beta_def; intro; elim H; intros _ H0; elim H0... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega