proposition: Lemma diagonal_included_r : forall n p, (n <= p)%nat -> snd (Dn p) <= snd (Dn n).
proof: Proof. intros n p H. induction H; simpl. right; reflexivity. apply Rle_trans with (r2 := snd (Dn m)). apply succ_included_r; apply diagonal_compat. assumption. Qed.
imports: Reals Lra