proposition: Lemma lemma_equalitysymmetric : forall A B, eq B A -> eq A B.
proof: Proof. intros. assert (eq A A) by (conclude cn_equalityreflexive). assert (eq A B) by (conclude cn_equalitytransitive). close. Qed.
imports: GeoCoq.Elements.OriginalProofs.euclidean_tactics