proposition: Lemma rho_ub_0 : forall h : TypeSpeed, (rho h < rho_ub h)%R.
proof: Proof. intros; unfold rho, rho_ub in |- *; apply Rmult_lt_compat_l; [ apply g_pos | generalize TypeSpeed_pos; intros; generalize (H h); clear H; intro H; generalize (Rinv_0_lt_compat h H); intro H1; generalize tan_MaxBank_ub; intro H2; generalize (Rmult_lt_compat_l (/ h) (tan MaxBank) tan_ub_MaxBank H1 H2); rewrite Rmult_comm; rewrite <- (Rmult_comm tan_ub_MaxBank); intro H3; assumption ]. Qed.
imports: Reals trajectory_const