proposition: Lemma nat_to_ring_Sn (n : nat) : nat_to_ring (S n) = plus (nat_to_ring n) one.
proof: Proof. case: n => [ | n] ; rewrite /nat_to_ring. rewrite sum_n_n sum_n_m_zero //. by rewrite plus_zero_l. rewrite sum_n_Sm //. by apply le_n_S, Nat.le_0_l. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis