proposition: Lemma PythFOk : forall A B, (PythF A B) * (PythF A B) =F= A*A + B*B.
proof: Proof. intros. unfold PythF, MulF, AddF, EqF;simpl. destruct A as [A HA];destruct B as [B HB];simpl. destruct (Pyth_f A B HA HB) as [C [HC1 HC2]]. destruct (prod_f A A HA HA) as [A2 HA2]. destruct (prod_f B B HB HB) as [B2 HB2]. assert (HC : Col O E C). destruct HC2;[apply Ps_Col;auto|subst;Col]. destruct (sum_f A2 B2) as [x Hx]. simpl. destruct (prod_f C C HC HC) as [C2 HC2']. simpl. assert (T:=PythOK O E E' A B C A2 B2 C2 HC1 HA2 HB2 HC2') . assert (x= C2) by (apply (sum_uniqueness O E E' A2 B2);auto). subst. destruct (prod_f C C) as [C2' HC2'']. simpl. apply (prod_uniqueness O E E' C C C2' C2);auto. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems