proposition: Lemma route_equiv_Origin : forall r r', r =r= r' <-> move r Point_O = move r' Point_O .
proof: Proof. split;intro H. - now rewrite H. - intro P;replace P with (translate (Point_x P) (Point_y P) Point_O). + repeat rewrite move_translate. rewrite H;reflexivity. + destruct P;simpl;unfold translate;f_equal. Qed.
imports: List ZArith Bool Relations Setoid Morphisms RelationClasses EMonoid Lia