proposition: Lemma ltp_to_lt : forall O E E' A B L C D M, Length O E E' A B L -> Length O E E' C D M -> LtP O E E' L M -> Lt A B C D.
proof: Proof. intros. assert(LeP O E E' L M). apply ltp_to_lep; auto. unfold Lt. split. apply(length_leP_le_1 O E E' A B C D L M); auto. intro. assert(HH:= length_eq_cong_2 O E E' A B C D L H H3). assert(L = M). { apply (length_uniqueness O E E' C D); auto. } subst M. unfold LtP in H1. ex_and H1 P. assert(~Col O E E' /\ Col O E L). { unfold Diff in H1. ex_and H1 X. unfold Sum in H5. unfold Ar2 in H5. spliter. tauto. } spliter. assert(HP:= diff_null O E E' L H5 H6). assert(P = O). apply(diff_uniqueness O E E' L L P O); auto. subst P. unfold Ps in H4. unfold Out in H4. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order