proposition: Lemma integer_0_1 : forall x, 0 < IZR x < 1 -> False.
proof: Proof. intros x [H0 H1]. apply lt_IZR in H0; apply lt_IZR in H1. lia. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Rsequence_subsequence Rpser_usual Reals Rsequence_tactics Rtactic Lra