Theorem: rescale_triangle_of_base_B (Pythagoras/euclid_VI.lean)

State before:
i : incidence_geometry
a b c d : point
L : line
n : ℕ
bL : online b L
cL : online c L
dL : online d L
hlen : length b d = ↑n * length b c
Bbcd : B b c d
aL : ¬online a L
⊢ area a b d = ↑n * area a b c
Tactic:
exact rescale_triangle_of_base_inductive a bL cL aL d dL hlen Bbcd
State after:
no goals