proposition: Lemma PythRel_exists : forall O E E', ~ Col O E E' -> forall A B, Col O E A -> Col O E B -> exists C, PythRel O E E' A B C.
proof: Proof. intros. assert_diffs. destruct (eq_dec_points O B). - subst. exists A. unfold PythRel. split. unfold Ar2;auto. left;auto. - destruct (perp_exists O E O) as [X HX]. auto. destruct (segment_construction_2 X O O B) as [B' [HB1 HB2]]. assert_diffs;auto. destruct (segment_construction_2 E O A B') as [C [HC1 HC2]]. auto. exists C. unfold PythRel. split. unfold Ar2. repeat split;auto. destruct HC1. auto using bet_col . apply bet_col in H3. Col. right. exists B'. split. assert (Perp O X O B). apply (perp_col1 O X O E B);Col. Perp. assert (Perp O B O B'). apply (perp_col1 O B O X B'). intro;treat_equalities. intuition. Perp. destruct HB1. apply bet_col in H6. Col. apply bet_col in H6. Col. Perp. split. Cong. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch16_coordinates