proposition: Lemma odd_S2n : forall n : nat, Nat.Odd n -> {p : nat | n = S (Nat.double p)}.
proof: Proof. intros n H_odd; exists (Nat.div2 n). apply Nat.Odd_double; assumption. Defined.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra