proposition: Lemma move_comm : forall r r' P , move r (move r' P) = move r' (move r P) .
proof: Proof. induction r as [| a r'];[reflexivity|]. - simpl;destruct a; intros;repeat rewrite move_translate;rewrite IHr';auto. Qed.
imports: List ZArith Bool Relations Setoid Morphisms RelationClasses EMonoid Lia