proposition: Lemma CS_seq_inv : Cauchy_prop (fun n => [--] (f n)).
proof: Proof. red in |- *; intros e H. elim (Hf e H); intros N Hn. exists N; intros m Hm. apply AbsSmall_minus. rstepr (f m[-]f N). auto. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)