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