proposition: Lemma nullsegment2 : forall A B, TCong A A B B.
proof: Proof. intros. unfold TCong;auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Elements.OriginalProofs.proposition_01 GeoCoq.Elements.OriginalProofs.lemma_congruenceflip GeoCoq.Elements.OriginalProofs.lemma_extension Classical