proposition: Lemma Rseq_alt_zip : forall An Bn, Rseq_alt (Rseq_zip An Bn) == Rseq_zip An (- Bn).
proof: Proof. intros An Bn n ; unfold Rseq_alt, Rseq_zip, Rseq_mult, Rseq_opp, Rseq_pow ; case (n_modulo_2 n) ; intros [p Hp] ; subst. rewrite pow_1_even ; apply Rmult_1_l. rewrite pow_1_odd ; ring. Qed.
imports: MyRIneq Rsequence_def