# ScarfPath / Primitive 声明迁移表

这是命名空间与声明名称的完整对应表。左列是原先的声明，右列是当前入口；证明方法、通用图论模块与坐标子命名空间的迁移也包含在内。使用方式见 [接口导览](scarf-primitive.md)。

## 固定颜色图

| 原声明 | 当前声明 |
| --- | --- |
| `IndexedLOrder.GiCell` | `ScarfPath.Cell` |
| `IndexedLOrder.GiRoomVertex` | `ScarfPath.IsRoomVertex` |
| `IndexedLOrder.GiDoorVertex` | `ScarfPath.IsDoorVertex` |
| `IndexedLOrder.GiVertex` | `ScarfPath.IsVertex` |
| `IndexedLOrder.GiEdge` | `ScarfPath.Edge` |
| `IndexedLOrder.GiEdge.symm` | `ScarfPath.Edge.symm` |
| `IndexedLOrder.GiEdge.left_vertex` | `ScarfPath.Edge.left_vertex` |
| `IndexedLOrder.GiEdge.right_vertex` | `ScarfPath.Edge.right_vertex` |
| `IndexedLOrder.GiRoomVertex.room` | `ScarfPath.IsRoomVertex.room` |
| `IndexedLOrder.GiDoorVertex.door` | `ScarfPath.IsDoorVertex.door` |
| `IndexedLOrder.GiEdge.irrefl` | `ScarfPath.Edge.irrefl` |
| `IndexedLOrder.GiGraph` | `ScarfPath.graph` |
| `IndexedLOrder.GiNeighbors` | `ScarfPath.neighbors` |
| `IndexedLOrder.mem_GiNeighbors` | `ScarfPath.mem_neighbors` |
| `IndexedLOrder.GiDegree` | `ScarfPath.degree` |
| `IndexedLOrder.GiEndpoint` | `ScarfPath.IsEndpoint` |
| `IndexedLOrder.not_room_of_door` | `ScarfPath.not_room_of_door` |
| `IndexedLOrder.not_colorful_of_door` | `ScarfPath.not_colorful_of_door` |
| `IndexedLOrder.not_GiRoomVertex_of_door` | `ScarfPath.not_IsRoomVertex_of_door` |
| `IndexedLOrder.not_door_of_room` | `ScarfPath.not_door_of_room` |
| `IndexedLOrder.not_GiDoorVertex_of_room` | `ScarfPath.not_IsDoorVertex_of_room` |
| `IndexedLOrder.isDoor_of_Doorof` | `ScarfPath.isDoor_of_Doorof` |
| `IndexedLOrder.GiRoomVertex_of_incident_typed_door` | `ScarfPath.isRoomVertex_of_incident_typed_door` |
| `IndexedLOrder.GiDegree_internalDoor` | `ScarfPath.degree_of_internalDoor` |
| `IndexedLOrder.GiDegree_typedNCRoom` | `ScarfPath.degree_of_typedNCRoom` |
| `IndexedLOrder.GiDegree_outsideDoor` | `ScarfPath.degree_of_outsideDoor` |
| `IndexedLOrder.GiDegree_colorfulRoom` | `ScarfPath.degree_of_colorfulRoom` |
| `IndexedLOrder.GiDegreeCharacterization` | `ScarfPath.DegreeCharacterization` |
| `IndexedLOrder.GiDegreeCharacterization_holds` | `ScarfPath.degree_characterization` |
| `IndexedLOrder.GiPathStructure` | `ScarfPath.PathStructure` |
| `IndexedLOrder.GiComponentStructure` | `ScarfPath.ComponentStructure` |
| `IndexedLOrder.GiPathStructure_of_degreeCharacterization` | `ScarfPath.pathStructure_of_degreeCharacterization` |
| `IndexedLOrder.GiComponentStructure_of_components_are_paths_or_cycles` | `ScarfPath.componentStructure_of_components_have_spanning_paths_or_cycles` |
| `IndexedLOrder.GiComponentStructure_holds` | `ScarfPath.component_structure` |

## Primitive 与坐标实现

| 原声明 | 当前声明 |
| --- | --- |
| `IndexedLOrder.ExtendedGoods` | `Primitive.ExtendedGoods` |
| `IndexedLOrder.toPrimitiveSet` | `Primitive.toPrimitiveSet` |
| `IndexedLOrder.toAlmostPrimitive` | `Primitive.toAlmostPrimitive` |
| `IndexedLOrder.fromGoods` | `Primitive.goods` |
| `IndexedLOrder.fromMissing` | `Primitive.missingColors` |
| `IndexedLOrder.associatedCell` | `Primitive.cell` |
| `IndexedLOrder.associatedCell_fst` | `Primitive.cell_fst` |
| `IndexedLOrder.associatedCell_snd` | `Primitive.cell_snd` |
| `IndexedLOrder.mem_toPrimitiveSet_inl` | `Primitive.mem_toPrimitiveSet_inl` |
| `IndexedLOrder.mem_toPrimitiveSet_inr` | `Primitive.mem_toPrimitiveSet_inr` |
| `IndexedLOrder.mem_toAlmostPrimitive_inl` | `Primitive.mem_toAlmostPrimitive_inl` |
| `IndexedLOrder.mem_toAlmostPrimitive_inr` | `Primitive.mem_toAlmostPrimitive_inr` |
| `IndexedLOrder.mem_fromGoods` | `Primitive.mem_goods` |
| `IndexedLOrder.mem_fromMissing` | `Primitive.mem_missingColors` |
| `IndexedLOrder.fromGoods_toPrimitiveSet` | `Primitive.goods_toPrimitiveSet` |
| `IndexedLOrder.fromMissing_toPrimitiveSet` | `Primitive.missingColors_toPrimitiveSet` |
| `IndexedLOrder.fromGoods_toAlmostPrimitive` | `Primitive.goods_toAlmostPrimitive` |
| `IndexedLOrder.fromMissing_toAlmostPrimitive` | `Primitive.missingColors_toAlmostPrimitive` |
| `IndexedLOrder.goods_slacks_disjoint` | `Primitive.goods_slacks_disjoint` |
| `IndexedLOrder.card_toPrimitiveSet` | `Primitive.card_toPrimitiveSet` |
| `IndexedLOrder.eq_toPrimitive_from_parts` | `Primitive.eq_toPrimitive_from_parts` |
| `IndexedLOrder.eq_toAlmost_from_parts` | `Primitive.eq_toAlmost_from_parts` |
| `IndexedLOrder.card_toPrimitiveSet_of_room` | `Primitive.card_toPrimitiveSet_of_room` |
| `IndexedLOrder.card_toAlmostPrimitive_of_door` | `Primitive.card_toAlmostPrimitive_of_door` |
| `IndexedLOrder.exists_insert_eq_of_subset_card_eq_succ` | `Primitive.exists_insert_eq_of_subset_card_eq_succ` |
| `IndexedLOrder.isRoomPrimitive` | `Primitive.IsRoomPrimitive` |
| `IndexedLOrder.isPrimitive` | `Primitive.IsPrimitive` |
| `IndexedLOrder.isPrimitiveNative` | `Primitive.IsPrimitiveNative` |
| `IndexedLOrder.isAlmostPrimitive` | `Primitive.IsAlmostPrimitive` |
| `IndexedLOrder.isAlmostPrimitiveNative` | `Primitive.IsAlmostPrimitiveNative` |
| `IndexedLOrder.room_to_roomPrimitive` | `Primitive.isRoomPrimitive_of_room` |
| `IndexedLOrder.primitive_to_room` | `Primitive.IsPrimitive.isRoom` |
| `IndexedLOrder.room_to_primitive` | `Primitive.isPrimitive_of_room` |
| `IndexedLOrder.isPrimitive_toPrimitiveSet_iff_room` | `Primitive.isPrimitive_toPrimitiveSet_iff_room` |
| `IndexedLOrder.primitive_eq_toPrimitive_from_parts` | `Primitive.primitive_eq_toPrimitive_from_parts` |
| `IndexedLOrder.primitive_from_parts` | `Primitive.primitive_from_parts` |
| `IndexedLOrder.primitive_to_nativePrimitive` | `Primitive.IsRoomPrimitive.isPrimitive` |
| `IndexedLOrder.nativePrimitive_to_primitive` | `Primitive.IsPrimitive.isRoomPrimitive` |
| `IndexedLOrder.isPrimitive_iff_native` | `Primitive.isRoomPrimitive_iff_isPrimitive` |
| `IndexedLOrder.door_to_almostPrimitive` | `Primitive.door_to_almostPrimitive` |
| `IndexedLOrder.almostPrimitive_to_door` | `Primitive.IsAlmostPrimitive.isDoor` |
| `IndexedLOrder.almostPrimitive_incident_room` | `Primitive.almostPrimitive_incident_room` |
| `IndexedLOrder.doorof_toAlmost_subset_toPrimitive` | `Primitive.doorof_toAlmost_subset_toPrimitive` |
| `IndexedLOrder.doorof_iff_subset_primitive` | `Primitive.doorof_iff_subset_primitive` |
| `IndexedLOrder.almostPrimitive_eq_toAlmost_from_parts` | `Primitive.almostPrimitive_eq_toAlmost_from_parts` |
| `IndexedLOrder.subset_toPrimitive_toAlmost_doorof` | `Primitive.subset_toPrimitive_toAlmost_doorof` |
| `IndexedLOrder.nativeAlmostPrimitive_to_almostPrimitive` | `Primitive.nativeAlmostPrimitive_to_almostPrimitive` |
| `IndexedLOrder.almostPrimitive_to_nativeAlmostPrimitive` | `Primitive.almostPrimitive_to_nativeAlmostPrimitive` |
| `IndexedLOrder.isAlmostPrimitive_iff_native` | `Primitive.isAlmostPrimitive_iff_native` |
| `IndexedLOrder.internal_almostPrimitive_two_incident_primitives` | `Primitive.internal_almostPrimitive_two_incident_primitives` |
| `IndexedLOrder.internal_almostPrimitive_exactly_two_incident_primitives` | `Primitive.internal_almostPrimitive_exactly_two_incident_primitives` |
| `IndexedLOrder.native_internal_almostPrimitive_exactly_two_incident_primitives` | `Primitive.native_internal_almostPrimitive_exactly_two_incident_primitives` |
| `IndexedLOrder.native_primitive_erase_mainLemma` | `Primitive.IsPrimitive.erase_incidence` |
| `IndexedLOrder.native_primitive_erase_replacement_mainLemma` | `Primitive.IsPrimitive.erase_replacement` |
| `IndexedLOrder.slackBoundary` | `Primitive.slackBoundary` |
| `IndexedLOrder.fromGoods_slackBoundary` | `Primitive.goods_slackBoundary` |
| `IndexedLOrder.fromMissing_slackBoundary` | `Primitive.missingColors_slackBoundary` |
| `IndexedLOrder.associatedCell_slackBoundary` | `Primitive.cell_slackBoundary` |
| `IndexedLOrder.slackBoundary_isAlmostPrimitive` | `Primitive.slackBoundary_isAlmostPrimitive` |
| `IndexedLOrder.slackBoundary_isAlmostPrimitiveNative` | `Primitive.slackBoundary_isAlmostPrimitiveNative` |
| `IndexedLOrder.slackBoundary_unique_incident_primitive` | `Primitive.slackBoundary_unique_incident_primitive` |
| `IndexedLOrder.slackBoundary_unique_incident_nativePrimitive` | `Primitive.slackBoundary_unique_incident_nativePrimitive` |
| `IndexedLOrder.boundary_almostPrimitive_eq_slackBoundary` | `Primitive.boundary_almostPrimitive_eq_slackBoundary` |
| `IndexedLOrder.boundary_almostPrimitive_unique_incident_primitive` | `Primitive.boundary_almostPrimitive_unique_incident_primitive` |
| `IndexedLOrder.native_boundary_almostPrimitive_unique_incident_primitive` | `Primitive.native_boundary_almostPrimitive_unique_incident_primitive` |
| `IndexedLOrder.almostPrimitive_incident_primitives_boundary_or_internal` | `Primitive.almostPrimitive_incident_primitives_boundary_or_internal` |
| `IndexedLOrder.native_almostPrimitive_incident_primitives_boundary_or_internal` | `Primitive.native_almostPrimitive_incident_primitives_boundary_or_internal` |
| `IndexedLOrder.almostPrimitive_subset_primitive_iff_doorof` | `Primitive.almostPrimitive_subset_primitive_iff_doorof` |
| `IndexedLOrder.primitiveReplacementStep` | `Primitive.ReplacementStep` |
| `IndexedLOrder.primitiveReplacementStep.symm` | `Primitive.ReplacementStep.symm` |
| `IndexedLOrder.replacementStep_has_common_door` | `Primitive.ReplacementStep.common_door` |
| `IndexedLOrder.common_door_gives_replacementStep` | `Primitive.common_door_gives_replacementStep` |
| `IndexedLOrder.internal_almostPrimitive_replacementStep` | `Primitive.internal_almostPrimitive_replacementStep` |
| `IndexedLOrder.extendedColoring` | `Primitive.extendedColoring` |
| `IndexedLOrder.extendedColoring_inl` | `Primitive.extendedColoring_inl` |
| `IndexedLOrder.extendedColoring_inr` | `Primitive.extendedColoring_inr` |
| `IndexedLOrder.image_extendedColoring_toPrimitiveSet` | `Primitive.image_extendedColoring_toPrimitiveSet` |
| `IndexedLOrder.full_color_primitive_iff_colorful_room` | `Primitive.full_color_primitive_iff_colorful_room` |
| `IndexedLOrder.isFullyColoredPrimitive` | `Primitive.IsFullyColored` |
| `IndexedLOrder.full_color_primitive_iff_colorful_associated_room` | `Primitive.full_color_primitive_iff_colorful_associated_room` |
| `IndexedLOrder.image_extendedColoring_toAlmostPrimitive` | `Primitive.image_extendedColoring_toAlmostPrimitive` |
| `IndexedLOrder.diff_image_eq_singleton_iff_allButColor_toPrimitiveSet` | `Primitive.diff_image_eq_singleton_iff_allButColor_toPrimitiveSet` |
| `IndexedLOrder.diff_image_eq_singleton_iff_allButColor_toAlmostPrimitive` | `Primitive.diff_image_eq_singleton_iff_allButColor_toAlmostPrimitive` |
| `IndexedLOrder.allButColor_primitive_iff_typed_associated_room` | `Primitive.allButColor_primitive_iff_typed_associated_room` |
| `IndexedLOrder.allButColor_almostPrimitive_iff_typed_associated_door` | `Primitive.allButColor_almostPrimitive_iff_typed_associated_door` |
| `IndexedLOrder.image_extendedColoring_slackBoundary` | `Primitive.image_extendedColoring_slackBoundary` |
| `IndexedLOrder.slackBoundary_GiDoorVertex` | `Primitive.slackBoundary_isDoorVertex` |
| `IndexedLOrder.fullyColoredPrimitive_GiRoomVertex` | `Primitive.fullyColoredPrimitive_isRoomVertex` |
| `IndexedLOrder.allButColorPrimitive_GiRoomVertex` | `Primitive.allButColorPrimitive_isRoomVertex` |
| `IndexedLOrder.allButColorAlmostPrimitive_GiDoorVertex` | `Primitive.allButColorAlmostPrimitive_isDoorVertex` |
| `IndexedLOrder.algorithm_incidence_to_GiEdge` | `Primitive.algorithm_incidence_to_edge` |
| `IndexedLOrder.scarfSplitReplacementStep` | `Primitive.SplitStep` |
| `IndexedLOrder.scarfSplitReplacementStep_replacementStep` | `Primitive.SplitStep.replacementStep` |
| `IndexedLOrder.scarfSplitReplacementStep_GiEdges` | `Primitive.SplitStep.edges` |
| `IndexedLOrder.scarfSplitReplacementStep_walk` | `Primitive.SplitStep.walk` |
| `IndexedLOrder.initial_scarf_step_to_GiEdge` | `Primitive.initial_edge` |
| `IndexedLOrder.initial_scarf_step_walk` | `Primitive.initial_walk` |
| `IndexedLOrder.ScarfAlgorithmTrace` | `Primitive.Trace` |
| `IndexedLOrder.ScarfAlgorithmTrace.terminal_colorful_room` | `Primitive.Trace.terminal_colorful_room` |
| `IndexedLOrder.scarfAlgorithmTrace_of_reachable_fullyColoredPrimitive` | `Primitive.Trace.nonempty_of_reachable` |
| `IndexedLOrder.scarfAlgorithmTrace_of_component_fullyColoredPrimitive` | `Primitive.Trace.nonempty_of_component` |
| `IndexedLOrder.scarfAlgorithmTrace_nonempty_iff_component_fullyColoredPrimitive` | `Primitive.Trace.nonempty_iff_component` |
| `IndexedLOrder.outsideDoor_endpoint_cell_eq_slackBoundary` | `Primitive.outsideDoor_endpoint_cell_eq_slackBoundary` |
| `IndexedLOrder.giVertex_of_GiDegree_eq_one` | `Primitive.isVertex_of_degree_eq_one` |
| `IndexedLOrder.scarfAlgorithmTrace_exists` | `Primitive.Trace.nonempty` |
| `IndexedLOrder.scarf_fullyColoredPrimitive_exists_via_trace` | `Primitive.exists_fullyColored_via_trace` |
| `IndexedLOrder.scarf_fullyColoredPrimitive_exists` | `Primitive.exists_fullyColored` |
| `IndexedLOrder.initial_scarf_primitive_from_boundary` | `Primitive.initial_primitive` |
| `IndexedLOrder.replacementStep_splits_through_almostPrimitive` | `Primitive.ReplacementStep.exists_face` |
| `IndexedLOrder.UtilityRealization` | `Primitive.Coordinate.Realization` |
| `IndexedLOrder.PositiveUtilityRealization` | `Primitive.Coordinate.PositiveRealization` |
| `IndexedLOrder.orderLowerSet` | `Primitive.Coordinate.orderLowerSet` |
| `IndexedLOrder.orderUtility` | `Primitive.Coordinate.orderUtility` |
| `IndexedLOrder.orderUtility_positive` | `Primitive.Coordinate.orderUtility_positive` |
| `IndexedLOrder.orderUtility_order_iff` | `Primitive.Coordinate.orderUtility_order_iff` |
| `IndexedLOrder.orderUtility_realization` | `Primitive.Coordinate.orderUtility_realization` |
| `IndexedLOrder.positiveOrderUtility_realization` | `Primitive.Coordinate.positiveOrderUtility_realization` |
| `IndexedLOrder.utilityVector` | `Primitive.Coordinate.utilityVector` |
| `IndexedLOrder.utilityVector_injective_of_realization` | `Primitive.Coordinate.utilityVector_injective_of_realization` |
| `IndexedLOrder.utilityImage` | `Primitive.Coordinate.utilityImage` |
| `IndexedLOrder.utilityImageEquiv` | `Primitive.Coordinate.utilityImageEquiv` |
| `IndexedLOrder.slackVector` | `Primitive.Coordinate.slackVector` |
| `IndexedLOrder.extendedCoordinatePoint` | `Primitive.Coordinate.extendedCoordinatePoint` |
| `IndexedLOrder.uniformSlackHeight` | `Primitive.Coordinate.uniformSlackHeight` |
| `IndexedLOrder.slackVector_self` | `Primitive.Coordinate.slackVector_self` |
| `IndexedLOrder.slackVector_of_ne` | `Primitive.Coordinate.slackVector_of_ne` |
| `IndexedLOrder.slackVector_other_coordinate_gt` | `Primitive.Coordinate.slackVector_other_coordinate_gt` |
| `IndexedLOrder.SlackHeightsDominateGoodsCoordinates` | `Primitive.Coordinate.SlackHeightsDominateGoodsCoordinates` |
| `IndexedLOrder.SlackBounds` | `Primitive.Coordinate.SlackBounds` |
| `IndexedLOrder.slackBounds_iff_heights_gt_coordinates` | `Primitive.Coordinate.slackBounds_iff_heights_gt_coordinates` |
| `IndexedLOrder.slackBounds_of_global_coordinate_bound` | `Primitive.Coordinate.slackBounds_of_global_coordinate_bound` |
| `IndexedLOrder.slackImage` | `Primitive.Coordinate.slackImage` |
| `IndexedLOrder.coordinateEnlargedSet` | `Primitive.Coordinate.coordinateEnlargedSet` |
| `IndexedLOrder.extendedCoordinatePoint_mem_coordinateEnlargedSet` | `Primitive.Coordinate.extendedCoordinatePoint_mem_coordinateEnlargedSet` |
| `IndexedLOrder.slackVector_injective_of_bounds` | `Primitive.Coordinate.slackVector_injective_of_bounds` |
| `IndexedLOrder.utilityVector_ne_slackVector_of_positive` | `Primitive.Coordinate.utilityVector_ne_slackVector_of_positive` |
| `IndexedLOrder.extendedCoordinatePoint_injective_of_realization` | `Primitive.Coordinate.extendedCoordinatePoint_injective_of_realization` |
| `IndexedLOrder.coordinateEnlargedSet_exists_preimage` | `Primitive.Coordinate.coordinateEnlargedSet_exists_preimage` |
| `IndexedLOrder.extendedCoordinateEquivCoordinateEnlargedSet` | `Primitive.Coordinate.extendedCoordinateEquivCoordinateEnlargedSet` |
| `IndexedLOrder.extendedCoordinatePoint_good` | `Primitive.Coordinate.extendedCoordinatePoint_good` |
| `IndexedLOrder.extendedCoordinatePoint_slack` | `Primitive.Coordinate.extendedCoordinatePoint_slack` |
| `IndexedLOrder.slackBounds_lt_slack_coordinate` | `Primitive.Coordinate.slackBounds_lt_slack_coordinate` |
| `IndexedLOrder.orderUtility_lt_uniformSlackHeight` | `Primitive.Coordinate.orderUtility_lt_uniformSlackHeight` |
| `IndexedLOrder.orderUtility_slackBounds` | `Primitive.Coordinate.orderUtility_slackBounds` |
| `IndexedLOrder.extendedCoordinateLt` | `Primitive.Coordinate.extendedCoordinateLt` |
| `IndexedLOrder.CoordinateValuesDefineLinearOrders` | `Primitive.Coordinate.DefinesLinearOrders` |
| `IndexedLOrder.SlackHeightsPairwiseDistinct` | `Primitive.Coordinate.SlackHeightsPairwiseDistinct` |
| `IndexedLOrder.utilityCoordinateValues` | `Primitive.Coordinate.utilityCoordinateValues` |
| `IndexedLOrder.utilityCoordinateValues_nonempty` | `Primitive.Coordinate.utilityCoordinateValues_nonempty` |
| `IndexedLOrder.utilityCoordinateBound` | `Primitive.Coordinate.utilityCoordinateBound` |
| `IndexedLOrder.utility_lt_utilityCoordinateBound` | `Primitive.Coordinate.utility_lt_utilityCoordinateBound` |
| `IndexedLOrder.perturbedSlackHeight` | `Primitive.Coordinate.perturbedSlackHeight` |
| `IndexedLOrder.perturbedSlackHeight_slackBounds` | `Primitive.Coordinate.perturbedSlackHeight_slackBounds` |
| `IndexedLOrder.perturbedSlackHeight_pairwiseDistinct` | `Primitive.Coordinate.perturbedSlackHeight_pairwiseDistinct` |
| `IndexedLOrder.utility_coordinate_injective` | `Primitive.Coordinate.utility_coordinate_injective` |
| `IndexedLOrder.extendedCoordinatePoint_coordinate_injective` | `Primitive.Coordinate.extendedCoordinatePoint_coordinate_injective` |
| `IndexedLOrder.coordinateValuesDefineLinearOrders_of_realization` | `Primitive.Coordinate.coordinateValuesDefineLinearOrders_of_realization` |
| `IndexedLOrder.exists_perturbedSlackHeights_for_coordinate_orders` | `Primitive.Coordinate.exists_perturbedSlackHeights_for_coordinate_orders` |
| `IndexedLOrder.exists_coordinateUtilityModel` | `Primitive.Coordinate.exists_model` |
| `IndexedLOrder.coordinateIndexedLOrder` | `Primitive.Coordinate.indexedLOrder` |
| `IndexedLOrder.extendedCoordinateLt_of_coord_lt` | `Primitive.Coordinate.extendedCoordinateLt_of_coord_lt` |
| `IndexedLOrder.extendedCoordinateLt_goods_of_original_lt` | `Primitive.Coordinate.extendedCoordinateLt_goods_of_original_lt` |
| `IndexedLOrder.original_lt_of_extendedCoordinateLt_goods` | `Primitive.Coordinate.original_lt_of_extendedCoordinateLt_goods` |
| `IndexedLOrder.extendedCoordinateLt_goods_iff` | `Primitive.Coordinate.extendedCoordinateLt_goods_iff` |
| `IndexedLOrder.coordinateGoods_le_of_original_le` | `Primitive.Coordinate.coordinateGoods_le_of_original_le` |
| `IndexedLOrder.original_le_of_coordinateGoods_le` | `Primitive.Coordinate.original_le_of_coordinateGoods_le` |
| `IndexedLOrder.coordinateGood_lt_slack_of_ne` | `Primitive.Coordinate.coordinateGood_lt_slack_of_ne` |
| `IndexedLOrder.coordinateSlack_lt_good` | `Primitive.Coordinate.coordinateSlack_lt_good` |
| `IndexedLOrder.coordinateSlack_lt_slack_of_ne` | `Primitive.Coordinate.coordinateSlack_lt_slack_of_ne` |
| `IndexedLOrder.isCoordinatePrimitive` | `Primitive.Coordinate.IsPrimitive` |
| `IndexedLOrder.nativePrimitive_to_coordinatePrimitive` | `Primitive.Coordinate.isPrimitive_of_native` |
| `IndexedLOrder.coordinatePrimitive_to_nativePrimitive` | `Primitive.Coordinate.IsPrimitive.to_native` |
| `IndexedLOrder.coordinatePrimitive_iff_native` | `Primitive.Coordinate.isPrimitive_iff_native` |
| `IndexedLOrder.coordinatePrimitive_erase_replacement_mainLemma` | `Primitive.Coordinate.IsPrimitive.erase_replacement` |

## 通用图论

| 原声明 | 当前声明 |
| --- | --- |
| `IndexedLOrder.simpleGraphDegreeAtMostTwo` | `PathComponents.DegreeAtMostTwo` |
| `IndexedLOrder.simpleGraphPathComponent` | `PathComponents.ComponentHasSpanningPath` |
| `IndexedLOrder.simpleGraphCycleComponent` | `PathComponents.ComponentHasSpanningCycle` |
| `IndexedLOrder.simpleGraphComponentsArePathsOrCycles` | `PathComponents.ComponentsHaveSpanningPathsOrCycles` |
| `IndexedLOrder.exists_maximal_component_path_of_degree_le_two` | `PathComponents.exists_maximal_component_path_of_degree_le_two` |
| `IndexedLOrder.maximal_component_path_no_escape_of_degree_le_two` | `PathComponents.maximal_component_path_no_escape_of_degree_le_two` |
| `IndexedLOrder.component_path_support_eq_component_of_no_escape` | `PathComponents.component_path_support_eq_component_of_no_escape` |
| `IndexedLOrder.component_cycle_of_maximal_path_closes` | `PathComponents.component_cycle_of_maximal_path_closes` |
| `IndexedLOrder.component_path_of_support_eq_component` | `PathComponents.component_path_of_support_eq_component` |
| `IndexedLOrder.simpleGraph_components_path_or_cycle_of_degree_le_two` | `PathComponents.components_have_spanning_paths_or_cycles_of_degree_le_two` |
| `IndexedLOrder.reachableComponentGraph` | `PathComponents.reachableComponent` |
| `IndexedLOrder.reachableComponentGraph_degree_eq` | `PathComponents.reachableComponent_degree` |