proposition: Lemma ub_nonincreasing_step:forall k alpha, ub alpha (S k) <= ub alpha k.
proof: Proof. intro k; induction k. intro alpha; stepr Qone; trivial; apply ub_is_in_base_interval_up. intros [d alpha']. rewrite ub_S_n; rewrite (ub_S_n k (Cons d alpha')); unfold hd, tl. destruct d as [ | | ]; set (u':=ub alpha' (S k)); set (u'':=ub alpha' k); generalize (IHk alpha'); clear IHk; intros IHk; fold u' u'' in IHk. assert (H_u'_one_nonneg: Zero <= u'+1). stepr (u'-(Qopp 1)); try ring; apply Qle_Qminus_Zero; subst u'; apply ub_is_in_base_interval_low. 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_u''_one_nonneg: Zero <= u''+1). stepr (u''-(Qopp 1)); try ring; apply Qle_Qminus_Zero; subst u''; apply ub_is_in_base_interval_low. 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. repeat rewrite as_Moebius_Q_L; trivial; natZ_numerals. apply Qmult_Qdiv_pos_Qle; auto. apply Qle_Zero_Qminus. stepr (4*(u''-u')). 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_u'_one_nonneg: Zero <= -u'+1). stepr (1-u'); try ring; apply Qle_Qminus_Zero; subst u'; apply ub_is_in_base_interval_up. 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_min_u''_one_nonneg: Zero <= -u''+1). stepr (1-u''); try ring; apply Qle_Qminus_Zero; subst u''; apply ub_is_in_base_interval_up. 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. repeat rewrite as_Moebius_Q_R; trivial; natZ_numerals; apply Qmult_Qdiv_pos_Qle; auto. apply Qle_Zero_Qminus. stepr (4*(u''-u')). 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*(u''-u')). apply Qle_mult_nonneg_nonneg; auto. apply Qle_Qminus_Zero; assumption. qnat_S 2; qnat_S 1; qnat_one; ring. Defined.
imports: digits lb