proposition: Lemma pythagoras_obtuse_or_per : forall O E E' A B C AC BC AB AC2 BC2 AB2 S2, O<>E -> Obtuse A C B \/ Per A C B -> 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' AC2 BC2 S2 -> LeP O E E' S2 AB2.
proof: Proof. intros. induction H0. { apply ltp_to_lep. apply (pythagoras_obtuse O E E' A B C AC BC AB AC2 BC2 AB2 S2); auto. } { assert(HH:= pythagoras O E E' A B C AC BC AB AC2 BC2 AB2 H H0 H1 H2 H3 H4 H5 H6). assert(S2 = AB2). { apply (sum_uniqueness O E E' AC2 BC2); auto. } subst S2. apply leP_refl. } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order