proposition: Lemma init_tr_cond_y : forall (h : TypeSpeed) (t : R), derive_pt (fun t : R => 0%R) t (init_tr_derivable_y h t) = (h * sin ((fun t : R => 0) t))%R.
proof: Proof. intros; reg. rewrite sin_0; ring. Qed.
imports: Reals trajectory_const rrho