proposition: Lemma thesis_5_7_9:forall k alpha, (ub alpha k) - (lb alpha k) <= 2/(k+1).
proof: Proof. intros k; induction k. intro alpha. unfold ub,lb. stepl 2; auto; stepr 2; auto; apply Qle_reflexive. assert (H_k_nonneg: 0 <= k). apply Z_to_Qle; apply inj_le; auto with arith. assert (H_k_one_pos: Zero < k + 1); [natq_zero; qnat_one; natq_S k; natq_S (S k); auto|]. assert (H_k_two_pos: Zero < k + 2 );[natq_zero; qnat_S 1; qnat_one; rewrite Qplus_assoc; natq_S k; natq_S (S k); auto|]. assert (H_k_three_pos: Zero < k + 3 ); [natq_zero; qnat_S 2; qnat_S 1; qnat_one; rewrite Qplus_assoc; natq_S k; natq_S (S k); auto|]. assert (H_k_two_div_k_one_pos: Zero < 2 /(k + 1));[unfold Qdiv; auto|]. intros [[ | | ] alpha']; generalize (IHk alpha'); clear IHk; rewrite ub_S_n; rewrite lb_S_n; unfold hd,tl; set (u'':=ub alpha' k); set (l'':=lb alpha' k); qnat_one; qnat_S k; intro IHk. assert (H_u''_one_nonneg: Zero <= u''+1); [ stepr (u''-(Qopp 1)); try ring; apply Qle_Qminus_Zero; subst u''; apply ub_is_in_base_interval_low|]. assert (H_u''_three_pos: Zero < u''+3); [ apply Qle_lt_trans with (u''+1); auto; apply Qlt_Zero_Qminus; stepr 2; auto; qnat_S 2; qnat_S 1; qnat_one; ring|]. assert (H_l''_one_nonneg: Zero <= l''+1); [ stepr (l''-(Qopp 1)); try ring; apply Qle_Qminus_Zero; subst l''; apply lb_is_in_base_interval_low|]. assert (H_l''_three_pos: Zero < l''+3); [apply Qle_lt_trans with (l''+1); auto; apply Qlt_Zero_Qminus; stepr 2; auto; qnat_S 2; qnat_S 1; qnat_one; ring|]. repeat rewrite as_Moebius_Q_L; trivial; natZ_numerals. rewrite Qminus_Qdiv; auto; case (Q_eq_dec l'' (Qopp 1)); intro H_l''. rewrite H_l''; rewrite H_l'' in IHk. assert (IHk_usable:Zero <= 2 - (u'' * k + u'' + k + 1)). apply Qle_Qminus_Zero; apply Qmult_resp_Qle_pos_r with ((k+Qone)^); auto; stepl (u''-(- Qone)); auto; qnat_one; generalize u''; intro x; field; auto. apply Qmult_Qdiv_pos_Qle; auto; apply Qle_Zero_Qminus. stepr (4*(2-(u''*k+u''+k+1))). apply Qle_mult_nonneg_nonneg; auto. qnat_S 3; qnat_S 2; qnat_S 1; qnat_one; ring. set (Psi_l :=fun x=> (2/(x+3))). assert (H_Psi_u''_pos:Zero < Psi_l u''); [ unfold Psi_l; unfold Qdiv; apply Qlt_mult_pos_pos; auto; apply Qinv_pos; auto|]. assert (H_Psi_l''_pos:Zero < Psi_l l''); [ unfold Psi_l; unfold Qdiv; apply Qlt_mult_pos_pos; auto; apply Qinv_pos; auto|]. apply Qlt_le_weak; apply Qle_lt_trans with (2/(k+3)). apply Qle_trans with ((2/(k+Qone))*((Psi_l u'')*(Psi_l l''))). stepl ((u'' - l'')*((Psi_l u'')*(Psi_l l''))). apply Qle_reg_mult_r; auto. unfold Psi_l; qnat_S 2; qnat_S 1; qnat_one; generalize u'' l'' H_u''_three_pos H_l''_three_pos; intros x y Hx Hy; field; repeat apply Qmult_resp_nonzero; auto. stepr ((2/(k + Qone))*(((k+Qone)/(k+2))*((k+2)/(k+3)))). apply Qle_reg_mult_l; auto. assert (H_Psi_l_nonincreasing:forall x y, (Qopp Qone) <=x -> x<=y -> Psi_l y <= Psi_l x). intros x y Hx_nonneg Hx_le_y; unfold Psi_l; apply Qmult_Qdiv_pos_Qle; match goal with | [ |- _ < ?X1 + _ ] => apply Qlt_le_trans with 2; auto; apply Qle_Zero_Qminus; stepr (X1- (Qopp Qone)); [apply Qle_Qminus_Zero | qnat_S 2; qnat_S 1; qnat_one; ring]; auto; apply Qle_trans with x; auto | [ |- _] => idtac end; apply Qle_Zero_Qminus; stepr (2*(y-x)); [apply Qle_mult_nonneg_nonneg; auto; apply Qle_Qminus_Zero; trivial | qnat_S 1; qnat_one; ring]. assert (H_Psi_l_1_min_k_1_plus_k:Psi_l ((1-k)/(1+k))= (k +1) / (k + 2)). unfold Psi_l; rewrite Qdiv_Qplus_Qmult; auto; rewrite Qdiv_Qdiv_Qmult_denominator; auto; [ apply Qmult_Qdiv | stepl (2*(k+2))]; auto; [ stepl (2*(k+2)) | | ]; auto; qnat_S 2; qnat_S 1; qnat_one; ring. assert (H__1_min_k_1_plus_k_ge_min_one:Qopp Qone <= (1-k)/(1+k)). apply Qle_Zero_Qminus; rewrite Qdiv_Qminus_Qmult; auto; unfold Qdiv; apply Qle_mult_nonneg_nonneg; auto; stepr 2; auto; qnat_S 1; qnat_one; ring. assert (H_Psi_l_min_k_k_two:Psi_l (-k/(k+2)) = (k+2)/(k+3)). unfold Psi_l; rewrite Qdiv_Qplus_Qmult; auto; rewrite Qdiv_Qdiv_Qmult_denominator; auto; [ apply Qmult_Qdiv | stepl (2*(k+3))]; auto; [ stepl (2*(k+3)) | | ]; auto; qnat_S 2; qnat_S 1; qnat_one; ring. assert (H_min_k_k_two_ge_min_one:Qopp Qone <= (-k)/(k+2)). apply Qle_Zero_Qminus; rewrite Qdiv_Qminus_Qmult; auto; unfold Qdiv; apply Qle_mult_nonneg_nonneg; auto; stepr 2; auto; qnat_S 1; qnat_one; ring. apply Qmult_Qle_compat; [ natq_one; rewrite <- H_Psi_l_1_min_k_1_plus_k; apply H_Psi_l_nonincreasing; auto; subst u''; apply thesis_5_7_2ii_u | rewrite <- H_Psi_l_min_k_k_two; apply H_Psi_l_nonincreasing; auto; subst l''; apply thesis_5_7_2i_l; auto | unfold Psi_l; auto | unfold Psi_l; auto ]. natq_one; generalize (k+1) (k+2) (k+3) H_k_one_pos H_k_two_pos H_k_three_pos; qnat_S 1; qnat_one; generalize (Qone+Qone); intros; field; auto. apply Qmult_Qdiv_pos; auto; apply Qlt_Zero_Qminus; stepr 2; auto; qnat_S 2; qnat_S 1; qnat_one; ring. assert (H_min_u''_one_nonneg: Zero <= -u''+1); [stepr (1-u''); try ring; apply Qle_Qminus_Zero; subst u''; apply ub_is_in_base_interval_up|]. assert (H_min_u''_three_pos: Zero < -u''+3); [ apply Qle_lt_trans with ((-u'')+1); auto;apply Qlt_Zero_Qminus; stepr 2; auto; qnat_S 2; qnat_S 1; qnat_one; ring|]. assert (H_min_l''_one_nonneg: Zero <= -l''+1); [stepr (1-l''); try ring; apply Qle_Qminus_Zero; subst l''; apply lb_is_in_base_interval_up|]. assert (H_min_l''_three_pos: Zero < -l''+3); [ apply Qle_lt_trans with ((-l'')+1); auto; apply Qlt_Zero_Qminus; stepr 2; auto; qnat_S 2; qnat_S 1; qnat_one; ring|]. repeat rewrite as_Moebius_Q_R; trivial; natZ_numerals. rewrite Qminus_Qdiv; auto; case (Q_eq_dec u'' 1); intro H_u''. rewrite H_u''; rewrite H_u'' in IHk. assert (IHk_usable:Zero<=2-(k+1-l''*k-l'')). apply Qle_Qminus_Zero; apply Qmult_resp_Qle_pos_r with ((k+Qone)^); auto; stepl (Qone - l''); auto; qnat_one; generalize l''; intro x; field; auto. apply Qmult_Qdiv_pos_Qle; auto; apply Qle_Zero_Qminus. stepr (4*(2-(k+1-l''*k-l''))). apply Qle_mult_nonneg_nonneg; auto. qnat_S 3; qnat_S 2; qnat_S 1; qnat_one; ring. set (Psi_r :=fun x=> (2/(-x+3))). assert (H_Psi_l''_pos:Zero < Psi_r l''); [ unfold Psi_r; unfold Qdiv; apply Qlt_mult_pos_pos; auto; apply Qinv_pos; auto|]. assert (H_Psi_u''_pos:Zero < Psi_r u''); [ unfold Psi_r; unfold Qdiv; apply Qlt_mult_pos_pos; auto; apply Qinv_pos; auto|]. apply Qlt_le_weak; apply Qle_lt_trans with (2/(k+3)). apply Qle_trans with ((2/(k+Qone))*((Psi_r l'')*(Psi_r u''))). stepl ((u'' - l'')*((Psi_r l'')*(Psi_r u''))). apply Qle_reg_mult_r; auto. unfold Psi_r; qnat_S 2; qnat_S 1; qnat_one; generalize l'' u'' H_min_l''_three_pos H_min_u''_three_pos; intros x y Hx Hy; field; repeat apply Qmult_resp_nonzero; auto. stepr ((2/(k + Qone))*(((k+Qone)/(k+2))*((k+2)/(k+3)))). apply Qle_reg_mult_l; auto. assert (H_Psi_r_nondecreasing:forall x y, y <= Qone -> x<=y -> Psi_r x <= Psi_r y). intros x y Hx_nonneg Hx_le_y; unfold Psi_r; apply Qmult_Qdiv_pos_Qle; match goal with | [ |- _ < Qopp ?X1 + _ ] => apply Qlt_le_trans with 2; auto; apply Qle_Zero_Qminus; stepr (Qone - X1); [apply Qle_Qminus_Zero | qnat_S 2; qnat_S 1; qnat_one; ring]; auto; apply Qle_trans with y; auto | [ |- _] => idtac end; apply Qle_Zero_Qminus; stepr (2*(y-x)); [apply Qle_mult_nonneg_nonneg; auto; apply Qle_Qminus_Zero; trivial | qnat_S 1; qnat_one; ring]. assert (H_Psi_r_k_min_1_k_plus_1:Psi_r ((k-1)/(k+1))=(k+1)/(k+2)). unfold Psi_r; rewrite <- Qdiv_Qopp_numerator; auto; rewrite Qdiv_Qplus_Qmult; auto; rewrite Qdiv_Qdiv_Qmult_denominator; auto; [ apply Qmult_Qdiv | stepl (2*(k+2))]; auto; [ stepl (2*(k+2)) | | ]; auto; qnat_S 2; qnat_S 1; qnat_one; ring. assert (H_k_min_1_k_plus_1_le_one: (k-1)/(k+1) <= Qone). apply Qle_Zero_Qminus; rewrite Qminus_Qdiv_Qmult; auto; unfold Qdiv; apply Qle_mult_nonneg_nonneg; auto; stepr 2; auto; qnat_S 1; qnat_one; ring. assert (H_Psi_r_k_k_two:Psi_r (k/(k+2))=(k+2)/(k+3)). unfold Psi_r; rewrite <- Qdiv_Qopp_numerator; auto; rewrite Qdiv_Qplus_Qmult; auto; rewrite Qdiv_Qdiv_Qmult_denominator; auto; [ apply Qmult_Qdiv | stepl (2*(k+3))]; auto; [ stepl (2*(k+3)) | | ]; auto; qnat_S 2; qnat_S 1; qnat_one; ring. assert (H_k_k_two_le_one: k/(k+2)<=Qone). apply Qle_Zero_Qminus; rewrite Qminus_Qdiv_Qmult; auto; unfold Qdiv; apply Qle_mult_nonneg_nonneg; auto; stepr 2; auto; qnat_S 1; qnat_one; ring. apply Qmult_Qle_compat; [ natq_one; rewrite <- H_Psi_r_k_min_1_k_plus_1; apply H_Psi_r_nondecreasing; auto; subst l''; apply thesis_5_7_2ii_l | rewrite <- H_Psi_r_k_k_two; apply H_Psi_r_nondecreasing; auto; subst u''; apply thesis_5_7_2i_u; auto | unfold Psi_r; auto | unfold Psi_r; auto ]. natq_one; generalize (k+1) (k+2) (k+3) H_k_one_pos H_k_two_pos H_k_three_pos; qnat_S 1; qnat_one; generalize (Qone+Qone); intros; field; auto. apply Qmult_Qdiv_pos; auto; apply Qlt_Zero_Qminus; stepr 2; auto; qnat_S 2; qnat_S 1; qnat_one; ring. assert (H_2k_1_pos: Zero<2*k+1); [apply Qle_lt_trans with (2*k); auto; apply Qlt_Zero_Qminus; stepr 1; auto; qnat_S 1; qnat_one; ring|]. repeat rewrite as_Moebius_Q_M; trivial; natZ_numerals. apply Qlt_le_weak; apply Qle_lt_trans with ((2/(k+1))/3). stepl ((u''-l'')/3). unfold Qdiv; apply Qle_reg_mult_r; auto. generalize u'' l''; intros x y; field; auto. rewrite Qdiv_Qdiv_Qmult_numerator; auto; apply Qmult_Qdiv_pos; auto; apply Qlt_Zero_Qminus; stepr (2*(2*k+1)); auto; qnat_S 3; qnat_S 2; qnat_S 1; qnat_one; ring. Defined.
imports: digits lb