proposition: Lemma length_existence : forall O E E' A B, ~ Col O E E' -> exists AB, Length O E E' A B AB.
proof: Proof. intros. assert(NEO : E <> O). intro. subst E. apply H. Col. assert(HH:= segment_construction_2 E O A B NEO). ex_and HH AB. exists AB. unfold Length. assert(AB = O \/ Out O E AB). induction(eq_dec_points AB O). left; assumption. right. repeat split; auto. assert(Col O E AB). induction H2. subst AB. Col. apply out_col. assumption. repeat split; Col. unfold LeP. induction H2. right; auto. left. unfold LtP. exists AB. repeat split. apply diff_A_O; Col. unfold Out in H2. tauto. auto. induction H0. right; assumption. left; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order