proposition: Lemma sequence_bound : forall n p, (n <= p)%nat -> (fst (Dn n)) <= Ln p <= (snd (Dn n)).
proof: Proof. intros n p H; split. left; eapply Rle_lt_trans with (r2 := fst (Dn p)). apply diagonal_included_l; apply H. apply Rlt_middle_l; apply diagonal_compat. left; apply Rlt_le_trans with (r2 := snd (Dn p)). apply Rlt_middle_r; apply diagonal_compat. apply diagonal_included_r; apply H. Qed.
imports: Reals Lra