proposition: Lemma MaxBank_encadr : (0 < MaxBank < PI / 4)%R.
proof: Proof. split. unfold MaxBank in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ prove_sup | apply Rinv_0_lt_compat; prove_sup ]. apply Rlt_trans with (PI_lb / 4)%R. unfold MaxBank in |- *; unfold Rdiv in |- *; apply Rmult_lt_reg_l with 100%R. prove_sup0. rewrite <- Rmult_comm; rewrite Rmult_assoc; rewrite <- Rinv_l_sym. rewrite Rmult_1_r; apply Rmult_lt_reg_l with 4%R. prove_sup. repeat rewrite (Rmult_comm 4); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. unfold PI_lb in |- *; prove_sup. discrR. discrR. unfold Rdiv in |- *; repeat rewrite <- (Rmult_comm (/ 4)); apply Rmult_lt_compat_l. apply Rinv_0_lt_compat; prove_sup. elim PI_approx; trivial. Qed.
imports: Reals trajectory_const rrho