proposition: Lemma gta_distincts : forall A B C D E F, GtA A B C D E F -> A<>B /\ C<>B /\ D<>E /\ F<>E /\ A <> C.
proof: Proof. intros A B C D E F Hgta. apply lta_distincts in Hgta. spliter. repeat split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2