proposition: Lemma lta_left_comm : forall A B C D E F, LtA A B C D E F -> LtA C B A D E F.
proof: Proof. unfold LtA. intros. spliter. split. apply lea_left_comm. assumption. intro. apply H0. apply conga_left_comm. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2