proposition: Lemma pythrelOO : forall O E E' C, PythRel O E E' O O C -> C = O.
proof: Proof. intros. unfold PythRel in H. spliter. induction H0. spliter. induction H1. auto. apply opp_midpoint in H1. unfold Midpoint in H1. spliter. apply cong_symmetry in H2. apply cong_identity in H2. auto. ex_and H0 B'. apply perp_distinct in H0. tauto. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems