proposition: Lemma pyth_context : forall O E E' A B C : Tpoint, ~Col O E E' -> exists AB BC AC AB2 BC2 AC2 SS, Col O E AB /\ Col O E BC /\ Col O E AC /\ Col O E AB2 /\ Col O E BC2 /\ Col O E AC2 /\ Length O E E' A B AB /\ Length O E E' B C BC /\ Length O E E' A C AC /\ Prod O E E' AB AB AB2 /\ Prod O E E' BC BC BC2 /\ Prod O E E' AC AC AC2 /\ Sum O E E' AB2 BC2 SS .
proof: Proof. intros. assert(Lab:=length_existence O E E' A B H). ex_and Lab AB. assert(Lbc:=length_existence O E E' B C H). ex_and Lbc BC. assert(Lac:=length_existence O E E' A C H). ex_and Lac AC. assert(Col O E AB /\ Col O E BC /\ Col O E AC). unfold Length in *; tauto. spliter. assert(Pab:= prod_exists O E E' H AB AB H3 H3). ex_and Pab AB2. assert(Pbc:= prod_exists O E E' H BC BC H4 H4). ex_and Pbc BC2. assert(Pac:= prod_exists O E E' H AC AC H5 H5). ex_and Pac AC2. assert(Col O E AB2 /\ Col O E BC2 /\ Col O E AC2). unfold Prod in *. unfold Ar2 in *. tauto. spliter. assert(HS:= sum_exists O E E' H AB2 BC2 H9 H10). ex_and HS SS. exists AB. exists BC. exists AC. exists AB2. exists BC2. exists AC2. exists SS. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order