proposition: Lemma thesis_5_7_2ii_l:forall (k:nat) alpha, lb alpha k <= (k-1)/(k+1).
proof: Proof. intro k; induction k; intros alpha. simpl; 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 < 1 + k ). rewrite Qplus_sym; 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. rewrite lb_S_n; destruct alpha as [d alpha']; destruct d; unfold hd,tl; generalize (IHk alpha'); clear IHk; intros IHk; qnat_one; qnat_S k; set (l':=lb alpha' k); fold l' in IHk. assert (H_min_l'_one_nonneg: Zero <= -l'+1). stepr (1-l'); try ring; apply Qle_Qminus_Zero; unfold l'; apply lb_is_in_base_interval_up. assert (H_l'_one_nonneg: Zero <= l'+1). stepr (l'-(Qopp 1)); try ring; apply Qle_Qminus_Zero; unfold 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. rewrite as_Moebius_Q_L; trivial; natZ_numerals. apply Qmult_Qdiv_pos_Qle; auto; apply Qle_Zero_Qminus; stepr (2*((-l'+1)+2*k)). apply Qle_mult_nonneg_nonneg; auto; apply Qle_plus_pos_pos; 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; unfold 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. assert (H_l'_one_nonneg: Zero <= l'+1). stepr (l'-(Qopp 1)); try ring; apply Qle_Qminus_Zero; unfold l'; apply lb_is_in_base_interval_low. rewrite as_Moebius_Q_R; trivial; natZ_numerals. apply Qmult_Qdiv_pos_Qle; auto; apply Qle_Zero_Qminus; stepr (2*((k-1)-l'*(k+1))). apply Qle_mult_nonneg_nonneg; auto; apply Qle_Qminus_Zero; apply Qmult_resp_Qle_pos_r with (Qinv (k+1)). apply Qinv_pos; auto. rewrite <- Qmult_assoc; rewrite Qmult_Qinv_r; auto; stepl l'; trivial; try ring. qnat_S k; qnat_S 2; qnat_S 1; qnat_one; ring. generalize IHk; clear IHk; subst l'. destruct k; rewrite as_Moebius_Q_M; natZ_numerals; intro IHk. unfold lb; stepr Zero; auto. set (l':=lb alpha' (S k)); fold l' in IHk. assert (H_pk_nonneg: 0 <= k). apply Z_to_Qle; apply inj_le; auto with arith. assert (H_min_l'_one_nonneg: Zero <= -l'+1). stepr (1-l'); try ring; apply Qle_Qminus_Zero; unfold l'; apply lb_is_in_base_interval_up. assert (H_min_l'_three_pos: Zero <= -l'+3). apply Qle_trans with (-l'+1); auto; apply Qle_plus_plus; try apply Qle_reflexive; apply Z_to_Qle; apply inj_le; auto. apply Qmult_Qdiv_pos_Qle; auto; apply Qle_Zero_Qminus. stepr (k*(-l'+3)+3*(-l'+1)). apply Qle_plus_pos_pos; apply Qle_mult_nonneg_nonneg; auto. qnat_S (S k); qnat_S k; qnat_S 2; qnat_S 1; qnat_one; [ ring | natq_S k; natq_S (S k); auto]. Defined.
imports: digits