proposition: Lemma r_stric_increasing : forall h1 h2 : TypeSpeed, (h1 < h2)%R -> (r h1 < r h2)%R.
proof: Proof. intros; unfold r in |- *; generalize (rho_strict_decreasing h1 h2 H); intro H0; generalize (Rinv_lt_contravar (rho h2) (rho h1) (Rmult_lt_0_compat (rho h2) (rho h1) (rho_pos h2) (rho_pos h1)) H0); intro; apply (Rmult_le_0_lt_compat h1 h2 (/ rho h1) (/ rho h2) (Rlt_le 0 h1 (TypeSpeed_pos h1)) (Rlt_le 0 (/ rho h1) (Rinv_0_lt_compat (rho h1) (rho_pos h1))) H H1). Qed.
imports: Reals trajectory_const