proposition: Lemma init_tr_cond_x : forall (h : TypeSpeed) (t : R), derive_pt (fun t : R => (h * t)%R) t (init_tr_derivable_x h t) = (h * cos ((fun t : R => 0) t))%R.
proof: Proof. intros; reg. rewrite cos_0; ring. Qed.
imports: Reals trajectory_const rrho