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