proposition: Lemma MinBeta_pos : (0 < MinBeta)%R.
proof: Proof. unfold MinBeta in |- *; unfold Rdiv in |- *. apply Rmult_lt_0_compat; [ prove_sup | apply Rinv_0_lt_compat; prove_sup ]. Qed.
imports: Reals trajectory_const rrho constants Omega