proposition: Lemma Rseq_zip_opp : forall An Bn, - Rseq_zip An Bn == Rseq_zip (- An) (- Bn).
proof: Proof. intros An Bn n ; unfold Rseq_zip, Rseq_opp ; case (n_modulo_2 n) ; intros [p Hp] ; reflexivity. Qed.
imports: MyRIneq Rsequence_def