proposition: Lemma tau_le_0_diverg : (tau (measure2state intr 0) (measure2state (tr evad) 0) 0 <= 0)%R -> (d intr evad <= RR (measure2state intr 0) (measure2state (tr evad) 0) T)%R.
proof: Proof. Proof with trivial. intro; rewrite <- d_distance; rewrite distance_sym; rewrite <- R_distance... cut (0 <= T)%R... intro; generalize (asymptotic_increase_tau (measure2state intr 0) (measure2state (tr evad) 0) 0 0 T H H0); intro... repeat rewrite Rplus_0_l in H1... left; apply Rlt_le_trans with MinT... apply MinT_is_pos... apply (cond_1 T)... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys ails_def math_prop tau ails trajectory measure2state ails_trajectory alarm