proposition: Lemma two_Sn : forall n, (2 * S n = S (S (2 * n)))%nat.
proof: Proof. intro n ; ring. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra