proposition: Lemma rho_strict_decreasing : forall h1 h2 : TypeSpeed, (h1 < h2)%R -> (rho h2 < rho h1)%R.
proof: Proof. intros; unfold rho in |- *; apply Rmult_lt_compat_l; [ apply g_pos | unfold Rdiv in |- *; apply Rmult_lt_compat_l; [ apply tan_MaxBank_pos | apply (Rinv_lt_contravar h1 h2 (Rmult_lt_0_compat h1 h2 (TypeSpeed_pos h1) (TypeSpeed_pos h2)) H) ] ]. Qed.
imports: Reals trajectory_const