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