proposition: Lemma pythrel_null : forall O E E' A B, PythRel O E E' A B O -> A = O /\ B = O.
proof: Proof. intros. unfold PythRel in H. spliter. induction H0. spliter. induction H1. split; auto. apply opp_midpoint in H1. unfold Midpoint in H1. spliter. apply cong_identity in H2. split; auto. ex_and H0 B'. apply cong_symmetry in H2. apply cong_identity in H2. subst B'. unfold Ar2 in H. spliter. apply perp_right_comm in H0. apply perp_not_col in H0. apply False_ind. apply H0. assert(O0 <> E0). intro. subst E0. apply H; Col. ColR. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems