proposition: Lemma cong_eq : forall A B C, Cong B C A A -> B=C.
proof: Proof. intros. destruct (classic (B=C)). assumption. assert (A<>A). apply axiom_nocollapse with B C;auto. intuition. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Elements.OriginalProofs.proposition_01 GeoCoq.Elements.OriginalProofs.lemma_congruenceflip GeoCoq.Elements.OriginalProofs.lemma_extension Classical