fact: Record Trajectory : Type := mkTrajectory {x : Differential; y : Differential; theta : Differential; phi : Differential; h : TypeSpeed; cond_x : forall t : R, derive_pt x t (cond_diff x t) = (h * cos (theta t))%R; cond_y : forall t : R, derive_pt y t (cond_diff y t) = (h * sin (theta t))%R; cond_phi : forall t : R, (- MaxBank <= phi t <= MaxBank)%R; cond_theta : forall t : R, derive_pt theta t (cond_diff theta t) = (g * (tan (phi t) / h))%R}.
imports: Reals trajectory_const rrho