Theoremsdiff_dist_adj, diff_dist_adj, dist_eq_zero_iff, dist_triangle, exists_path_of_dist, exists_walk_length_eq_dist, exists_walk_length_eq_edist, one_lt_dist_of_ne_of_not_adj, pos_dist_of_ne, coe_dist_eq_edist, dist_anti, dist_eq_zero_iff, dist_triangle_left, dist_triangle_right, exists_path_of_dist, exists_walk_length_eq_dist, exists_walk_length_eq_edist, of_dist_ne_zero, one_lt_dist_of_ne_of_not_adj, pos_dist_of_ne, edist_le, exists_adj_adj_not_adj_ne, isPath_of_length_eq_dist, dist_bot, dist_comm, dist_eq_one_iff_adj, dist_eq_sInf, dist_eq_zero_iff_eq_or_not_reachable, dist_eq_zero_of_not_reachable, dist_le, dist_ne_zero_iff_ne_and_reachable, dist_self, dist_top, dist_top_of_ne, edist_anti, edist_bot, edist_bot_of_ne, edist_comm, edist_eq_one_iff_adj, edist_eq_sInf, edist_eq_top_of_not_reachable, edist_eq_zero_iff, edist_le, edist_le_one_iff_adj_or_eq, edist_ne_top_iff_reachable, edist_pos_of_ne, edist_self, edist_top, edist_top_of_ne, edist_triangle, exists_walk_of_dist_ne_zero, exists_walk_of_edist_eq_coe, exists_walk_of_edist_ne_top, length_eq_dist_of_subwalk, nonempty_of_pos_dist, reachable_of_edist_ne_top | 56 |