proposition: Lemma AlertRange_pos : (0 < AlertRange)%R.
proof: Proof. unfold AlertRange in |- *; prove_sup. Qed.
imports: Bool Reals trajectory_const trajectory_def constants ycngftys ycngstys ails_def math_prop tau ails trajectory measure2state ails_trajectory