fact: Fixpoint move (r:route) (P:Point) : Point := match r with | nil => P | North :: r' => move r' (translate 0 1 P) | East :: r' => move r' (translate 1 0 P) | South :: r' => move r' (translate 0 (-1) P) | West :: r' => move r' (translate (-1) 0 P) end.
imports: List ZArith Bool Relations Setoid Morphisms RelationClasses EMonoid Lia