proposition: Lemma lt_to_ltp : forall O E E' A B L C D M, Length O E E' A B L -> Length O E E' C D M -> Lt A B C D -> LtP O E E' L M.
proof: Proof. intros. induction(eq_dec_points L M). { subst M. apply length_cong in H0. apply length_cong in H. unfold Lt in H1. spliter. apply False_ind. apply H2; CongR. } { assert(Le A B C D). { apply lt__le; auto. } assert(HH:= length_leP_le_2 O E E' A B C D L M H H0 H3). unfold LeP in HH. induction HH. { assumption. } { contradiction. } } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order