proposition: Lemma Tcong_reflexive: forall A B, TCong A B A B.
proof: Proof. intros. unfold TCong. left. 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