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