proposition: Lemma Rseq_shift_shifts: forall Un n, Rseq_shifts Un (S n) == Rseq_shift (Rseq_shifts Un n).
proof: Proof. intros Un n k ; unfold Rseq_shift, Rseq_shifts ; f_equal ; apply plus_n_Sm. Qed.
imports: MyRIneq Rsequence_def