Theorem: not_B_of_short (Pythagoras/euclid_I_extras.lean)

State before:
i : incidence_geometry
a b c : point
hlen : length a b < length a c
hBacb : B a c b
⊢ False
Tactic:
rw [(length_sum_of_B hBacb).symm] at hlen
State after:
i : incidence_geometry
a b c : point
hlen : length a c + length c b < length a c
hBacb : B a c b
⊢ False

State before:
i : incidence_geometry
a b c : point
hlen : length a c + length c b < length a c
hBacb : B a c b
⊢ False
Tactic:
linarith [length_nonneg c b]
State after:
no goals