proposition: Lemma pythagoras : forall O E E' A B C AC BC AB AC2 BC2 AB2, O <> E -> 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 AB2.
proof: Proof. intros. assert(~Col O E E' /\ Col O E AB2 /\ Col O E AC2 /\ Col O E BC). unfold Prod in *. spliter. unfold Ar2 in H4 ,H5 ,H6. repeat split; tauto. spliter. induction(col_dec A C B). assert(HH:=l8_9 A C B H0 H11). induction HH. subst C. assert(AB = BC). apply(length_uniqueness O E E' A B). assumption. apply length_sym. assumption. subst BC. assert(AB2 = BC2). apply(prod_uniqueness O E E' AB AB); auto. subst BC2. assert(AC = O). apply(length_uniqueness O E E' A A). assumption. apply length_id_2; assumption. subst AC. assert(AC2=O). apply(prod_uniqueness O E E' O O). assumption. apply prod_0_l; Col. subst AC2. apply sum_O_B; Col. subst C. assert(AB = AC). apply(length_uniqueness O E E' A B). assumption. assumption. subst AC. assert(AB2 = AC2). apply(prod_uniqueness O E E' AB AB); auto. subst AC2. assert(BC = O). apply(length_uniqueness O E E' B B). assumption. apply length_id_2; assumption. subst BC. assert(BC2=O). apply(prod_uniqueness O E E' O O). assumption. apply prod_0_l; Col. subst BC2. apply sum_A_O; Col. assert(exists X : Tpoint, Col A B X /\ Perp A B C X). apply(l8_18_existence A B C); Col. ex_and H12 P. assert(Perp_at P A B C P). apply(l8_14_2_1b_bis A B C P P H13); Col. assert(Bet A P B /\ A <> P /\ B <> P). apply(l11_47 A B C P H0). Perp. spliter. assert(HL1:= length_existence O E E' A P H7). assert(HL2:= length_existence O E E' B P H7). ex_and HL1 AP. ex_and HL2 BP. assert(Sum O E E' AP BP AB). apply(triangular_equality_bis O E E' A P B AP BP AB); auto. apply length_sym. assumption. assert(Prod O E E' AB AP AC2). apply(l15_7_1 O E E' A B C P AB AC AP AC2 H H0); Perp. assert(Prod O E E' AB BP BC2). eapply(l15_7_1 O E E' B A C P AB BC); Perp. apply length_sym;auto. assert(HD:=distr_l O E E' AB AP BP AB AC2 BC2 AB2 H20 H21 H22 H6). assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order