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