proposition: Lemma Rseq_shifts_fusion : forall An k m, (Rseq_shifts (Rseq_shifts An k) m == Rseq_shifts An (k + m))%Rseq.
proof: Proof. intros ; unfold Rseq_shifts ; intro ; rewrite Nat.add_assoc ; reflexivity. Qed.
imports: MyRIneq Rsequence_def