proposition: Lemma north_south_simpl : forall r r', r++ North::South::r' =r= r++r'.
proof: Proof. induction r as [|a r'];simpl. - intro r';rewrite north_south_0;reflexivity. - intros r1;now rewrite IHr' . Qed.
imports: List ZArith Bool Relations Setoid Morphisms RelationClasses EMonoid Lia