proposition: Lemma lb_lt_ub_pointwise:forall k alpha, lb alpha k < ub alpha k.
proof: Proof. intros k; induction k. intro alpha. unfold ub,lb. apply Qlt_Zero_Qminus; stepr 2; auto. intros [[ | | ] alpha']; generalize (IHk alpha'); clear IHk; rewrite ub_S_n; rewrite lb_S_n; unfold hd,tl; set (u':=ub alpha' k); set (l':=lb alpha' k); intro IHk. assert (H_u'l': Zero < u'- l'); [apply Qlt_Qminus_Zero; assumption |]. 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_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; auto; apply Qlt_Zero_Qminus; stepr (4*(u'-l')); auto; qnat_S 3; qnat_S 2; qnat_S 1; qnat_one; ring. assert (H_u'l': Zero < u'- l'); [apply Qlt_Qminus_Zero; assumption |]. 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_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; auto; apply Qlt_Zero_Qminus; stepr (4*(u'-l')); auto; qnat_S 3; qnat_S 2; qnat_S 1; qnat_one; ring. repeat rewrite as_Moebius_Q_M; trivial; natZ_numerals. unfold Qdiv; apply Qlt_reg_mult_pos_r; auto. Defined.
imports: digits lb