proposition: Lemma sum_power_series : forall n (f : Rat -> Prop) a a', n > 0 -> (exists v, f v) -> (forall v1 v2, f v1 -> f v2 -> v1 == v2) -> (forall v, f v -> ~1 <= v) -> sumList_rel (fun i : nat => expRat_rel f i) (getNats 0 n) a -> ratMult_rel (ratSubtract_rel (eqRat 1) (expRat_rel f n)) (ratInverse_rel (ratSubtract_rel (eqRat 1) f)) a' -> a == a'.
proof: Proof. intuition. destruct H0. assert (sumList_rel (fun i => ratMult_rel f (expRat_rel f i)) (getNats O n) (x * a)). eapply ratMult_sumList_rel_distrib. eapply H3. unfold expRat_rel. intuition. rewrite H5; eauto. rewrite H6; eauto. intuition. trivial. trivial. assert (ratSubtract a (x * a) == ratSubtract 1 (expRat x n)). eapply ratSubtract_series_map; eauto. intuition. unfold expRat_rel, ratMult_rel in *. simpl in *. rewrite H6; eauto. rewrite H7; eauto. eapply eqRat_refl. intuition. eapply expRat_eqRat_compat; eauto. unfold expRat_rel. intuition. rewrite H7; eauto. unfold ratMult_rel, expRat_rel. intuition. rewrite H6; eauto. rewrite H7; eauto. eapply eqRat_refl. intuition. eapply expRat_eqRat_compat; eauto. intuition. eapply expRat_eqRat_compat; eauto. intuition. unfold expRat_rel, ratMult_rel in *. rewrite H7. 2:{ eauto. } 2:{ intuition. } rewrite ratMult_comm. eapply ratMult_small_le. case_eq (bleRat x 1); intuition. exfalso. eapply H2. eauto. eapply bleRat_total. trivial. unfold expRat_rel; intuition. eapply leRat_trans. eapply eqRat_impl_leRat. eapply H8. eauto. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply H7. eauto. } eapply expRat_le. case_eq (bleRat x 1); intuition. exfalso. eapply H2. eauto. eapply bleRat_total; trivial. lia. unfold ratMult_rel, expRat_rel. intuition. eapply leRat_trans. eapply eqRat_impl_leRat. eapply H8. eauto. intuition. eapply expRat_eqRat_compat. eauto. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply H7. eauto. intuition. eapply expRat_eqRat_compat. eauto. } eapply ratMult_leRat_compat. intuition. eapply expRat_le. case_eq (bleRat x 1); intuition. exfalso. eapply H2. eauto. eapply bleRat_total; trivial. lia. unfold expRat_rel; intuition. simpl. intuition. unfold ratMult_rel, ratSubtract_rel, expRat_rel, ratInverse_rel in *. intuition. rewrite H7; eauto. destruct n; try lia. simpl. eapply ratMult_eqRat_compat; eauto. eapply expRat_eqRat_compat; eauto. unfold ratMult_rel, ratSubtract_rel, expRat_rel, ratInverse_rel in H4. rewrite H4. 2:{ intuition. rewrite H8. rewrite <- H7. eapply eqRat_refl. eauto. } 2:{ intuition. eapply ratInverse_eqRat_compat. 2:{ rewrite H7. eapply eqRat_refl. eapply eqRat_refl. eauto. } intuition. eapply H2. eauto. apply ratSubtract_0_inv. trivial. } rewrite <- (ratMult_1_l a) in H6 at 1. eapply (@eqRat_ratMult_same_r (ratSubtract 1 x)). intuition. eapply H2; eauto. eapply ratSubtract_0_inv; trivial. rewrite ratMult_assoc. rewrite ratInverse_prod_1. rewrite ratMult_1_r. rewrite ratMult_comm. rewrite ratMult_ratSubtract_distrib_r. trivial. intuition. eapply H2. eauto. eapply ratSubtract_0_inv; trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation