proposition: Lemma power_series_limit_2 : forall (f : nat -> Rat -> Prop) a, rat_inf_limit f a -> (forall n v, f n v -> ~ 1 <= v) -> ~ 1 <= a -> (forall n, exists v, f n v) -> (forall n v1 v2, f n v1 -> f n v2 -> v1 == v2) -> rat_inf_limit (fun n => sumList_rel (fun i => expRat_rel (f n) i) (getNats O n)) (ratInverse (ratSubtract 1 a)).
proof: Proof. intuition. eapply (@rat_inf_limit_trans _ (fun n => (ratMult_rel (ratSubtract_rel (eqRat 1) (expRat_rel (f n) n)) (ratInverse_rel (ratSubtract_rel (eqRat 1) (f n)))))). unfold rat_inf_limit_2, inf_limit_2. intuition. exists (S O). intuition. destruct (H2 n'). eapply leRat_trans. eapply eqRat_impl_leRat. rewrite <- ratIdentityIndiscernables. eapply sum_power_series. assert (n' > O). lia. eapply H9. econstructor. eapply H8. eapply H3. intuition. eapply H0. eapply H9. trivial. trivial. trivial. eapply rat0_le_all. eapply rat_inf_limit_eq. eapply rat_inf_limit_product. unfold left_total, ratSubtract_rel, expRat_rel. intuition. destruct (H2 n). exists (ratSubtract 1 (expRat x n)). intuition. eapply ratSubtract_eqRat_compat; eauto. symmetry. eapply H6. trivial. unfold left_total, ratInverse_rel, ratSubtract_rel. intuition. destruct (H2 n). exists (ratInverse (ratSubtract 1 x)). intuition. eapply ratInverse_eqRat_compat. intuition. eapply H0. eauto. eapply ratSubtract_0_inv. trivial. symmetry. eapply H5; intuition. eapply rat_inf_limit_difference. unfold left_total; intuition. exists 1; intuition. unfold left_total, expRat_rel; intuition. destruct (H2 n). exists (expRat x n). intuition. eapply expRat_eqRat_compat; eauto. eapply rat_inf_limit_const. eapply eqRat_refl. intuition. rewrite <- H4. rewrite H5. intuition. eapply rat_inf_limit_exp_0. eauto. trivial. trivial. eapply rat_inf_limit_ratInverse. eapply rat_inf_limit_difference. unfold left_total; intuition. econstructor. eapply eqRat_refl. unfold left_total; intuition. eapply rat_inf_limit_const. eapply eqRat_refl. intuition. rewrite <- H4. rewrite H5. intuition. eauto. intuition. eapply H1. eapply ratSubtract_0_inv. trivial. eapply eqRat_refl. unfold left_total; intuition. destruct (H2 n). exists (ratSubtract 1 x). unfold ratSubtract_rel; intuition. eapply ratSubtract_eqRat_compat; eauto. rewrite ratSubtract_0_r. rewrite ratMult_1_l. intuition. unfold left_total, ratMult_rel, ratSubtract_rel, expRat_rel, ratInverse_rel. intuition. destruct (H2 n). exists ((ratSubtract 1 (expRat x n)) * (ratInverse (ratSubtract 1 x))). intuition. eapply ratMult_eqRat_compat. symmetry. eapply H5; intuition. eapply expRat_eqRat_compat. eauto. symmetry. eapply H6. intuition. eapply ratSubtract_eqRat_compat; intuition. eauto. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat Arith