proposition: Lemma tan_ub_MaxBank_pos : (0 < tan_ub_MaxBank)%R.
proof: Proof. apply Rlt_trans with tan_lb_MaxBank; [ apply tan_lb_MaxBank_pos | apply Rlt_trans with (tan MaxBank); [ apply tan_MaxBank_lb | apply tan_MaxBank_ub ] ]. Qed.
imports: Reals trajectory_const