proposition: Lemma Pyth_f : forall A B, Col O E A -> Col O E B -> {C | PythRel O E E' A B C /\ (Ps O E C \/ C = O)}.
proof: Proof. intros. intros; apply constructive_definite_description; rewrite <- unique_existence. split. assert(HE := PythRel_exists O E E' ncolOEE' A B H H0). ex_and HE C. assert(HC:Col O E C). unfold PythRel in *. spliter. unfold Ar2 in H1. tauto. induction(out_dec O E C). exists C. split; auto. left. unfold Ps. apply l6_6; auto. induction(eq_dec_points C O). subst C. exists O. split. auto. right;auto. assert(HH:= opp_exists O E E' ncolOEE' C HC). ex_and HH C'. exists C'. split. apply (opp_pythrel _ _ _ _ _ C); auto. left. unfold Ps. apply opp_midpoint in H4. unfold Midpoint in H4. spliter. unfold Out. repeat split. intro. subst C'. apply cong_identity in H5. contradiction. intro. rewrite H6 in *. apply H1;Col. apply not_out_bet in H2. apply(l5_2 C O C' E H3 H4); Between. Col. unfold uniqueness. intros. spliter. apply (PythRel_uniqueness O E E' A B); auto. induction H4; induction H3. left. split; auto. subst y. apply pythrel_null in H2. spliter. subst A. subst B. assert(HH:= pythrelOO O E E' x H1). subst x. unfold Ps in H4. unfold Out in H4. tauto. subst x. apply pythrel_null in H1. spliter. subst A. subst B. assert(HH:= pythrelOO O E E' y H2). subst y. unfold Ps in H3. unfold Out in H3. tauto. right. subst y. apply pythrel_null in H2. spliter. subst A. subst B. assert(HH:= pythrelOO O E E' x H1). assumption. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems