fact: Definition Omega (a : R) : bool := match Rle_dec (PI / 2) a with | left _ => match Rle_dec a (3 * (PI / 2)) with | left _ => true | right _ => false end | right _ => false end.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega