+ elim daemon.*)
+qed.
+
+definition max: ∀R:real.R → R → R.
+ intros (R x y);
+ apply (lim R (max_seq R x y));
+ apply cauchy_max_seq.
+qed.
+
+definition abs \def λR:real.λx:R. max R x (-x).
+
+lemma comparison:
+ ∀R:real.∀f,g:nat→R. is_cauchy_seq ? f → is_cauchy_seq ? g →
+ (∀n:nat.f n ≤ g n) → lim ? f ? ≤ lim ? g ?.
+ [ assumption
+ | assumption
+ | intros;
+ elim daemon
+ ].
+qed.
+
+definition to_zero ≝
+ λR:real.λn.
+ -(inv R (sum_field R (S n))
+ (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))).
+
+axiom is_cauchy_seq_to_zero: ∀R:real. is_cauchy_seq ? (to_zero R).
+
+lemma technical1: ∀R:real.lim R (to_zero R) (is_cauchy_seq_to_zero R) = 0.
+ intros;
+ unfold lim;
+ elim daemon.
+qed.