proposition: Theorem Alembert_C3 : forall (An:nat -> R) (x:R), (forall n:nat, An n <> 0) -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 -> { l:R | Pser An x l }.
proof: Proof. intros; destruct (total_order_T x 0) as [[Hlt|Heq]|Hgt]. - cut (x <> 0). + intro; apply AlembertC3_step1; assumption. + red; intro; rewrite H1 in Hlt; elim (Rlt_irrefl _ Hlt). - apply AlembertC3_step2; assumption. - cut (x <> 0). + intro; apply AlembertC3_step1; assumption. + red; intro; rewrite H1 in Hgt; elim (Rlt_irrefl _ Hgt). Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra