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