proposition: Lemma prop_47 : forall O E E' A B C AC BC AB AC2 BC2 AB2, O <> E -> Per B A C -> Length O E E' A B AB -> Length O E E' A C AC -> Length O E E' B C BC -> Prod O E E' AC AC AC2 -> Prod O E E' BC BC BC2 -> Prod O E E' AB AB AB2 -> Sum O E E' AB2 AC2 BC2.
proof: Proof. intros O E E' A B C AC BC AB AC2 BC2 AB2. intros. apply pythagoras with B C A AB AC BC; trivial; apply length_sym; assumption. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions