proposition: Lemma rho_lb_pos : forall h : TypeSpeed, (0 < rho_lb h)%R.
proof: Proof. intros; unfold rho_lb in |- *; apply Rmult_lt_0_compat; [ apply g_pos | replace (tan_lb_MaxBank / h)%R with (tan_lb_MaxBank * / h)%R; [ rewrite Rmult_comm; generalize TypeSpeed_pos; intro H; generalize (H h); clear H; intro H; generalize (Rinv_0_lt_compat h H); intro H0; apply Rmult_lt_0_compat; [ assumption | apply tan_lb_MaxBank_pos ] | auto ] ]. Qed.
imports: Reals trajectory_const