proposition: Lemma same_abscissa_col : forall O E S U1 U2 A AX AY B BY C CY, Cd O E S U1 U2 A AX AY -> Cd O E S U1 U2 B AX BY -> Cd O E S U1 U2 C AX CY -> Col A B C.
proof: Proof. intros O E S U1 U2 A AX AY B BY C CY HCdA HCdB HCdC. destruct HCdA as [HCs [H [[PXA [HProjpA HCongA]] H']]]; clear H; clear H'. destruct HCdB as [H [H' [[PXB [HProjpB HCongB]] H'']]]; clear H; clear H'; clear H''. destruct HCdC as [H [H' [[PXC [HProjpC HCongC]] H'']]]; clear H; clear H'; clear H''. assert (HDiff1 : O <> E) by (unfold Cs in *; spliter; auto). assert (HColAX : Col O E AX) by (apply l4_13 with S U1 PXA; Cong; apply projp_col with A; auto). eapply col_cong_3_cong_3_eq in HCongB; [| | |apply HCongA]; treat_equalities; auto. eapply col_cong_3_cong_3_eq in HCongC; [| | |apply HCongA]; treat_equalities; auto. clear HCongA; elim (eq_dec_points A PXA); intro HDiff2; treat_equalities; [apply projp2_col with S U1; auto|]. eapply projp2_col in HProjpB; [|apply HProjpA]. eapply projp2_col in HProjpC; [|apply HProjpA]. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths