proposition: Lemma is_length_exists : forall O E E' X Y, ~ Col O E E' -> exists XY, Is_length O E E' X Y XY.
proof: Proof. intros O E E' X Y HNC. elim (eq_dec_points X Y); intro HXY; [treat_equalities; exists O; left; apply length_id_2; assert_diffs; auto| destruct (length_existence O E E' X Y) as [XY HLength]; Col; exists XY; left; auto]. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order