proposition: Lemma Tcong_symmetric: forall A B C D, TCong A B C D -> TCong C D A B.
proof: Proof. intros. unfold TCong in *. destruct H. left. apply cong_sym. assumption. right;intuition. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Elements.OriginalProofs.proposition_01 GeoCoq.Elements.OriginalProofs.lemma_congruenceflip GeoCoq.Elements.OriginalProofs.lemma_extension Classical