proposition: Lemma Rseq_zip_extract_evens : forall Un Vn, Rseq_zip Un Vn ⋅ extractor_mult_2 == Un.
proof: Proof. intros Un Vn n ; unfold Rseq_zip, extracted, extractor_mult_2 ; simpl ; case (n_modulo_2 (n + (n + 0))) ; intros [p Hp]. f_equal ; lia. apply False_ind ; lia. Qed.
imports: Reals Rsequence_def Rsequence_facts Lia Lra