proposition: Lemma thesis_5_7_2i_u:forall k alpha, ~(ub alpha k = 1) -> ub alpha k <= k/(k+2).
proof: Proof. intro k; induction k; intros alpha H_nonzero. apply False_ind; apply H_nonzero; trivial. rewrite ub_S_n. rewrite ub_S_n in H_nonzero. assert (H_k_one_pos: Zero < k + Qone ). natq_S k; natq_zero; apply Z_to_Qlt; apply inj_lt; apply lt_O_Sn. assert (H_k_nonneg: 0 <= k). apply Z_to_Qle; apply inj_le; auto with arith. assert (H_2k_3_nonneg: Qone <= 2 * k + 3). apply Qle_Zero_Qminus; stepr (2*(k+1)); [ apply Qle_mult_nonneg_nonneg; auto | qnat_S 2; qnat_S 1; qnat_one; ring ]. destruct alpha as [[ | | ] alpha']; unfold hd,tl; unfold hd,tl in H_nonzero; qnat_one; qnat_S k; set (u':=ub alpha' k). 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. rewrite as_Moebius_Q_L; trivial; natZ_numerals. apply Qmult_Qdiv_pos_Qle; auto. apply Qle_Zero_Qminus. stepr (2*((2*k+3)-u')). apply Qle_mult_nonneg_nonneg; auto. apply Qle_Qminus_Zero. apply Qle_trans with Qone; auto; subst u'; apply ub_is_in_base_interval_up. qnat_S 2; qnat_S 1; qnat_one; ring. case (Q_eq_dec u' 1); intro H_u'. fold u' in H_nonzero. apply False_ind; apply H_nonzero; rewrite H_u'; rewrite as_Moebius_Q_R; qZ_numerals; auto. generalize (IHk alpha' H_u'); fold u'; clear IHk; intro IHk. 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. rewrite as_Moebius_Q_R; trivial; natZ_numerals. apply Qmult_Qdiv_pos_Qle; auto; apply Qle_Zero_Qminus; stepr (2*(k-u'*(k+2))). apply Qle_mult_nonneg_nonneg; auto. apply Qle_Qminus_Zero. apply Qmult_resp_Qle_pos_r with (Qinv (k+2)); auto. rewrite <- Qmult_assoc; rewrite Qmult_Qinv_r; auto. stepl u'; trivial; try ring. qnat_S 2; qnat_S 1; qnat_one; ring. generalize H_nonzero; clear H_nonzero; repeat rewrite as_Moebius_Q_M; natZ_numerals; intros H_nonzero; fold u' in H_nonzero. apply Qle_trans with (1/3). apply Qmult_Qdiv_pos_Qle; auto; apply Qle_Zero_Qminus; stepr (3*(1-u')). apply Qle_mult_nonneg_nonneg; auto; apply Qle_Qminus_Zero; subst u'; apply ub_is_in_base_interval_up. qnat_S 2; qnat_S 1; qnat_one; ring. apply Qmult_Qdiv_pos_Qle; auto; apply Qle_Zero_Qminus. stepr (2*k). apply Qle_mult_nonneg_nonneg; auto; apply Qle_Qminus_Zero; subst u'; apply ub_is_in_base_interval_up. qnat_S 2; qnat_S 1; qnat_one; ring. Defined.
imports: digits lb