proposition: Lemma lb_lt_ub:forall n k alpha, lb alpha n < ub alpha k.
proof: Proof. intros n k alpha. case (le_lt_dec n k); intro H_nk. apply Qle_lt_trans with (lb alpha k). apply lb_nondecreasing; trivial. apply lb_lt_ub_pointwise. apply Qlt_le_trans with (ub alpha n). apply lb_lt_ub_pointwise. apply ub_nonincreasing; apply lt_le_weak; trivial. Defined.
imports: digits lb