proposition: Lemma diagonal_not_in : forall n p, (n <= p)%nat -> ~ (fst (Dn p) <= Rn n <= snd (Dn p)).
proof: Proof. intros n p H. induction H; simpl. destruct n; simpl; apply succ_not_in; [assumption|apply diagonal_compat]. intros Hn; destruct Hn as [Hl Hr]. apply IHle; split. eapply Rle_trans; [|apply Hl]. apply succ_included_l; apply diagonal_compat. eapply Rle_trans; [apply Hr|]. apply succ_included_r; apply diagonal_compat. Qed.
imports: Reals Lra