Function match_midp_perp_cong

dd.py:212–224

Match midp M A B, perp O M A B => cong O A O B.

(
    g: gh.Graph,
    g_matcher: Callable[str, list[tuple[gm.Point, ...]]],
    theorem: pr.Theorem,
)

def match_midp_perp_cong(
    g: gh.Graph,
    g_matcher: Callable[str, list[tuple[gm.Point, ...]]],
    theorem: pr.Theorem,
) -> Generator[dict[str, gm.Point], None, None]:
  """Match midp M A B, perp O M A B => cong O A O B."""
  for m, a, b in g.all_midps():
    ab = g._get_line(a, b)
    for l in m.neighbors(gm.Line):
      if g.check_perpl(l, ab):
        for o in l.neighbors(gm.Point):
          if o != m:
            yield dict(zip('ABMO', [a, b, m, o]))


def match_cyclic_eqangle_cong(