proposition: Lemma cong_sym : forall A B C D, Cong A B C D -> Cong C D A B.
proof: Proof. intros. apply (cn_congruencetransitive C D A B A B). assumption. apply (cn_congruencereflexive). Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Elements.OriginalProofs.proposition_01 GeoCoq.Elements.OriginalProofs.lemma_congruenceflip GeoCoq.Elements.OriginalProofs.lemma_extension Classical