proposition: Lemma lta_dec : forall A B C D E F, LtA A B C D E F \/ ~ LtA A B C D E F.
proof: Proof. intros A B C D E F. elim(conga_dec A B C D E F). { intro. right. unfold LtA. intro. spliter. auto. } intro. elim(lea_dec A B C D E F). { intro. left. split; auto. } intro. right. unfold LtA. intro. spliter. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2