proposition: Lemma pythrel_not_null : forall O E E' A B C, C <> O -> PythRel O E E' A B C -> A <> O \/ B <> O.
proof: Proof. intros. unfold PythRel in H0. spliter. unfold Ar2 in H0; spliter. induction H1. spliter. left. intro. subst A. induction H5. subst C. tauto. subst B. apply opp_midpoint in H5. unfold Midpoint in H5. spliter. apply cong_symmetry in H5. apply cong_identity in H5. subst C. tauto. ex_and H1 B'. right. intro. subst B. apply perp_distinct in H1. 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