proposition: Lemma inv_inf_1 : forall x, x <> 0%nat -> /INR x <= 1.
proof: Proof. intros x Hx0. assert (H : (INR x > 0)) by intuition. assert (H1 : (INR x >= 1)). induction x. destruct Hx0. reflexivity. replace 1 with (0 + 1) by intuition. rewrite S_INR. apply Rplus_ge_compat. intuition. intuition. rewrite <- Rinv_1. apply Rle_Rinv. lra. assumption. intuition. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Rsequence_subsequence Rpser_usual Reals Rsequence_tactics Rtactic Lra