proposition: Lemma r_ub_0 : forall h : TypeSpeed, (r h < r_ub h)%R.
proof: Proof. intros; unfold r, r_ub in |- *; generalize (rho_lb_0 h); intro H; generalize (Rmult_lt_0_compat (rho_lb h) (rho h) (rho_lb_pos h) (rho_pos h)); intro H0; generalize (Rinv_lt_contravar (rho_lb h) (rho h) H0 H); intro H1; generalize (Rmult_lt_compat_l h (/ rho h) (/ rho_lb h) (TypeSpeed_pos h) H1); intro H2; assumption. Qed.
imports: Reals trajectory_const