proposition: Lemma Cauchy_fun_seq_Lim_char : forall a b Hab (Hinc : included (Compact Hab) J), Feq (Compact Hab) Cauchy_fun_seq_Lim_IR (Cauchy_fun_seq_Lim _ _ _ _ _ (conv a b Hab Hinc)).
proof: Proof. intros. FEQ. simpl in |- *. apply Lim_wd'; intros; simpl in |- *; algebra. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions