proposition: Lemma north_south_0 : forall r, North::South::r =r= r.
proof: Proof. intro r; change ((North::South::nil)++ r =r= r). setoid_replace (North :: South :: nil) with (@nil direction); [reflexivity |route_eq_tac ]. Qed.
imports: List ZArith Bool Relations Setoid Morphisms RelationClasses EMonoid Lia