Theorem: para_implies_eq_area_of_same_base (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a b c d : point
L M : line
aM : online a M
dM : online d M
bL : online b L
cL : online c L
pLM : para L M
⊢ area a b c = area d b c
Tactic:
exact eq_area_of_eq_base aM bL cL dM bL cL pLM rfl
State after:
no goals