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