fact: Record EvaderTrajectory : Type := mkEvaderTrajectory {tr : Trajectory; tr_cond1 : forall t : R, x tr t = (x tr 0 + h tr * t)%R; tr_cond2 : forall t : R, y tr t = y tr 0%R; tr_cond3 : forall t : R, theta tr t = 0%R; tr_cond4 : forall t : R, phi tr t = 0%R}.
imports: Reals trajectory_const rrho