proposition: Lemma CS_seq_recip : Cauchy_prop CS_seq_recip_seq.
proof: Proof. red in |- *; intros d Hd. elim (Hf ((d[*]e[*]e) [/]TwoNZ)); [ intros K HK | apply pos_div_two; repeat apply mult_resp_pos; auto ]. exists (Nat.max K N); intros n Hn. apply AbsSmall_cancel_mult with (f (Nat.max K N)). apply less_leEq_trans with e; auto with arith. apply AbsSmall_cancel_mult with (f n). apply less_leEq_trans with e; eauto with arith. unfold CS_seq_recip_seq in |- *. elim lt_le_dec; intro; simpl in |- *. exfalso; apply Nat.le_ngt with N n; eauto with arith. elim lt_le_dec; intro; simpl in |- *. exfalso; apply Nat.le_ngt with N (Nat.max K N); eauto with arith. rstepr (f (Nat.max K N)[-]f n). apply AbsSmall_leEq_trans with (d[*]e[*]e). apply mult_resp_leEq_both. apply less_leEq; apply mult_resp_pos; auto. apply less_leEq; auto. apply mult_resp_leEq_lft. auto with arith. apply less_leEq; auto. auto with arith. auto with arith. rstepr (f (Nat.max K N)[-]f K[+](f K[-]f n)). apply AbsSmall_eps_div_two. auto with arith. apply AbsSmall_minus; apply HK. eauto with arith. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)