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