proposition: Lemma thesis_5_7_2i_l:forall (k:nat) alpha, ~(lb alpha k = Qopp 1) -> (-k)/(k+2) <= lb alpha k.
proof: Proof. intro k; induction k; intros alpha H_nonzero. apply False_ind; apply H_nonzero; trivial. rewrite lb_S_n; rewrite lb_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_two_pos: Zero < k + 2 ). stepr ((k+Qone)+Qone); [ natq_S k; natq_S (S k); natq_zero; auto | qnat_S 1; qnat_one; ring]. 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 (l':=lb alpha' k). fold l' in H_nonzero. case (Q_eq_dec l' (Qopp 1)); intro H_l'. apply False_ind; apply H_nonzero; rewrite H_l'; rewrite as_Moebius_Q_L; qZ_numerals; auto. generalize (IHk alpha' H_l'); fold l'; clear IHk; intro IHk. 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. generalize H_nonzero; clear H_nonzero; rewrite as_Moebius_Q_L; trivial; natZ_numerals; intros H_nonzero. apply Qmult_Qdiv_pos_Qle; auto; apply Qle_Zero_Qminus; stepr (2*(l'*(k+2)-(-k))). apply Qle_mult_nonneg_nonneg; auto; apply Qle_Qminus_Zero; apply Qmult_resp_Qle_pos_r with (Qinv (k+2)). apply Qinv_pos; auto. rewrite <- Qmult_assoc; rewrite Qmult_Qinv_r; auto. stepr l'; trivial; try ring. 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. 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 Qlt_le_weak; 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_R; trivial; natZ_numerals. apply Qmult_Qdiv_pos_Qle; auto; apply Qle_Zero_Qminus; stepr (2*((l'+3)+2*k)). apply Qle_mult_nonneg_nonneg; auto. qnat_S 2; qnat_S 1; qnat_one; ring. rewrite as_Moebius_Q_M; natZ_numerals; 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. apply Qle_trans with ((-Qone)/3). apply Qmult_Qdiv_pos_Qle; auto; apply Qle_Zero_Qminus; stepr (2*k); auto; qnat_S 2; qnat_S 1; qnat_one; ring. apply Qmult_Qdiv_pos_Qle; auto; apply Qle_Zero_Qminus; stepr (3*(l'+1)). apply Qle_mult_nonneg_nonneg; auto. qnat_S 2; qnat_S 1; qnat_one; ring. Defined.
imports: digits