proposition: Lemma l15_7_2 : forall O E E' A B C H AB AC AH AC2, O<>E -> Per A C B -> Perp_at H C H A B -> Length O E E' A B AB -> Length O E E' A C AC -> Length O E E' A H AH -> Prod O E E' AB AH AC2 -> Prod O E E' AC AC AC2.
proof: Proof. intros. destruct(l15_7 O E E' A B C H AB AC AH AC2 H0 H1 H2 H3 H4 H5). apply H8. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order