proposition: Lemma integer_INR_div : forall b, b <> O -> / INR b * INR (fact b) = INR (fact (b - 1)).
proof: Proof. intros b Hb0. destruct b. destruct Hb0. reflexivity. rewrite fact_simpl. rewrite mult_INR. field_simplify. simpl. rewrite Nat.sub_0_r. reflexivity. INR_solve. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Rsequence_subsequence Rpser_usual Reals Rsequence_tactics Rtactic Lra