proposition: Lemma lb_nondecreasing_steps:forall n k alpha, lb alpha n <= lb alpha (k+n).
proof: Proof. intros [|n] k. intros; replace (k+0)%nat with k; trivial; apply lb_is_in_base_interval_low. induction k. intro alpha; apply Qle_reflexive. replace (S k +S n)%nat with (S (k+S n))%nat; trivial; intros [d alpha']; rewrite (lb_S_n n (Cons d alpha')); rewrite lb_S_n; unfold hd, tl. destruct d. apply as_Moebius_Q_L_nondecreasing; [ apply lb_is_in_base_interval_low | apply lb_is_in_base_interval_up | apply Qle_trans with (lb alpha' (S n)); trivial; apply lb_nondecreasing_step]. apply as_Moebius_Q_R_nondecreasing; [ apply lb_is_in_base_interval_low | apply lb_is_in_base_interval_up | apply Qle_trans with (lb alpha' (S n)); trivial; apply lb_nondecreasing_step]. apply as_Moebius_Q_M_nondecreasing; [ apply lb_is_in_base_interval_low | apply lb_is_in_base_interval_up | apply Qle_trans with (lb alpha' (S n)); trivial; apply lb_nondecreasing_step]. Defined.
imports: digits