proposition: Lemma lb_is_in_base_interval:forall k alpha, - Qone <= lb alpha k /\ lb alpha k <= Qone.
proof: Proof. intro k; induction k; intro alpha. split; unfold lb; natq_one; try rewrite <- Z_to_Qopp; apply Z_to_Qle; auto with zarith. destruct alpha as [[ | | ] alpha']; generalize (IHk alpha'); clear IHk; rewrite lb_S_n; unfold hd, tl; set (l':=lb alpha' k); intros [IHk_1 IHk_2]. assert (H_l'_one_nonneg: Zero <= l'+1). stepr (l'-(Qopp 1)); try ring; apply Qle_Qminus_Zero; auto. 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. assert (H_2l'_two_nonneg: Zero <= 2*l'+2). stepr (2*(l'+1)); [|qZ_numerals; ring]; apply Qle_mult_nonneg_nonneg; auto. assert (H_l'_two_nonneg: Zero <= l'+2). apply Qle_trans with (l'+1); auto; apply Qle_plus_plus; try apply Qle_reflexive; apply Z_to_Qle; apply inj_le; auto. rewrite as_Moebius_Q_L; trivial; natZ_numerals. split; apply Qmult_resp_Qle_pos_r with (l'+3); auto. stepr (l'-1). apply Qle_Zero_Qminus; stepr (2*l'+2); auto; qnat_S 2; qnat_S 1; qnat_one; ring. generalize (l'-1) (l'+3) H_l'_three_pos; intros; field; auto. stepl (l'-1). apply Qle_Zero_Qminus; stepr 4; auto; qnat_S 3; qnat_S 2; qnat_S 1; qnat_one; ring. generalize (l'-1) (l'+3) H_l'_three_pos; intros; field; auto. assert (H_min_l'_one_nonneg: Zero <= -l'+1). stepr (1-l'); try ring; apply Qle_Qminus_Zero; auto. 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_2_min_l'_two_nonneg: Zero <= 2*(-l')+2). stepr (2*(-l'+1)); [|qZ_numerals; ring]; apply Qle_mult_nonneg_nonneg; auto. rewrite as_Moebius_Q_R; trivial; natZ_numerals. split; apply Qmult_resp_Qle_pos_r with (-l'+3); auto. stepr (l'+1). apply Qle_Zero_Qminus; stepr 4; auto; qnat_S 3; qnat_S 2; qnat_S 1; qnat_one; ring. generalize (l'+1) (-l'+3) H_min_l'_three_pos; intros; field; auto. stepl (l'+1). apply Qle_Zero_Qminus; stepr (2*(-l')+2); auto; qnat_S 2; qnat_S 1; qnat_one; ring. generalize (l'+1) (-l'+3) H_min_l'_three_pos; intros; field; auto. rewrite as_Moebius_Q_M; natZ_numerals. split; apply Qmult_resp_Qle_pos_r with 3; auto; [ stepr l' | stepl l']. apply Qle_trans with (-Qone); auto; apply Qlt_le_weak; apply Qlt_Zero_Qminus; stepr 2; auto. generalize l'; intro; field; auto. apply Qle_trans with Qone; auto; apply Qlt_le_weak; apply Qlt_Zero_Qminus; stepr 2; auto. generalize l'; intro; field; auto. Defined.
imports: digits