proposition: Lemma route_compose : forall r r' P, move (r++r') P = move r' (move r P).
proof: Proof. induction r as [|d s IHs]; simpl; [auto | destruct d; intros;rewrite IHs;auto]. Qed.
imports: List ZArith Bool Relations Setoid Morphisms RelationClasses EMonoid Lia