proposition: Lemma tan_lb_MaxBank_pos : (0 < tan_lb_MaxBank)%R.
proof: Proof. unfold tan_lb_MaxBank in |- *; unfold Rdiv in |- *; apply Rmult_lt_reg_l with 10%R. prove_sup. rewrite Rmult_0_r; rewrite <- Rmult_comm; rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ prove_sup | discrR ]. Qed.
imports: Reals trajectory_const