Theorem: not_para_of_online_online (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a : point
L M : line
hL : online a L
hM : online a M
⊢ ¬para L M
Tactic:
simp_rw [para, not_forall, not_or, not_not]
State after:
i : incidence_geometry
a : point
L M : line
hL : online a L
hM : online a M
⊢ ∃ x, online x L ∧ online x M

State before:
i : incidence_geometry
a : point
L M : line
hL : online a L
hM : online a M
⊢ ∃ x, online x L ∧ online x M
Tactic:
exact ⟨ a, hL, hM ⟩
State after:
no goals