proposition: Lemma lb_nondecreasing_step:forall k alpha, lb alpha k <= lb alpha (S k).
proof: Proof. intro k; induction k. intro alpha; stepl (Qopp 1); trivial; apply lb_is_in_base_interval_low. intros [d alpha']; rewrite lb_S_n; rewrite (lb_S_n (S k) (Cons d alpha')); unfold hd, tl. destruct d as [ | | ]; set (l':=lb alpha' (S k)); set (l'':=lb alpha' k); generalize (IHk alpha'); clear IHk; intros IHk; fold l' l'' in IHk. 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 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 Qle_lt_trans with (l''+1); auto; apply Qlt_Zero_Qminus; stepr 2; auto; qnat_S 2; qnat_S 1; qnat_one; ring. repeat rewrite as_Moebius_Q_L; trivial; natZ_numerals. apply Qmult_Qdiv_pos_Qle; auto. apply Qle_Zero_Qminus. stepr (4*(l'-l'')). apply Qle_mult_nonneg_nonneg; auto. apply Qle_Qminus_Zero; assumption. qnat_S 3; 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_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. repeat rewrite as_Moebius_Q_R; trivial; natZ_numerals. apply Qmult_Qdiv_pos_Qle; auto. apply Qle_Zero_Qminus. stepr (4*(l'-l'')). apply Qle_mult_nonneg_nonneg; auto. apply Qle_Qminus_Zero; assumption. qnat_S 3; qnat_S 2; qnat_S 1; qnat_one; ring. do 2 rewrite as_Moebius_Q_M; natZ_numerals. apply Qmult_Qdiv_pos_Qle; auto. apply Qle_Zero_Qminus. stepr (3*(l'-l'')). apply Qle_mult_nonneg_nonneg; auto. apply Qle_Qminus_Zero; assumption. qnat_S 2; qnat_S 1; qnat_one; ring. Defined.
imports: digits