proposition: Lemma not_and_lta : forall A B C D E F, ~ (LtA A B C D E F /\ LtA D E F A B C).
proof: Proof. intros. intro. unfold LtA in *. spliter. assert(CongA A B C D E F). apply lea_asym. assumption. assumption. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2