proposition: Lemma theta_inv : forall t : R, (0 <= t)%R -> (thetat intr 0 - rho_vi * t <= thetat intr t)%R /\ (thetat intr t <= thetat intr 0 + rho_vi * t)%R.
proof: Proof. Proof with trivial. generalize (dtheta_rho intr); intros; split... unfold thetat in |- *; cut (derivable (fun y : R => (- rho_vi * y)%R)); [ intro X | reg ]... cut (forall z : R, derive_pt (fun y : R => (- rho_vi * y)%R) z (X z) = (- rho_vi)%R); [ intro | intro; reg ]... apply Rplus_le_reg_l with (- theta intr 0)%R... replace (- theta intr 0 + (theta intr 0 - rho_vi * t))%R with (- rho_vi * t - - rho_vi * 0)%R; [ idtac | ring ]... replace (- theta intr 0 + theta intr t)%R with (theta intr t - theta intr 0)%R; [ idtac | ring ]... apply (IAF_var (theta intr) (fun y : R => (- rho_vi * y)%R) 0 t (cond_diff (theta intr)) X H0)... intros; rewrite (H1 c); unfold rho_vi in |- *; unfold vi in |- *; elim (H c); intros H4 _; assumption... unfold thetat in |- *; cut (derivable (fun y : R => (rho_vi * y)%R)); [ intro X | reg ]... cut (forall z : R, derive_pt (fun y : R => (rho_vi * y)%R) z (X z) = rho_vi); [ intro | intro; reg ]... apply Rplus_le_reg_l with (- theta intr 0)%R... replace (- theta intr 0 + (theta intr 0 + rho_vi * t))%R with (rho_vi * t - rho_vi * 0)%R; [ idtac | ring ]... replace (- theta intr 0 + theta intr t)%R with (theta intr t - theta intr 0)%R; [ idtac | ring ]... apply (IAF_var (fun y : R => (rho_vi * y)%R) (theta intr) 0 t X (cond_diff (theta intr)) H0)... intros; rewrite (H1 c); unfold rho_vi in |- *; unfold vi in |- *; elim (H c)... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega