proposition: Lemma lemma_inequalitysymmetric : forall A B, neq A B -> neq B A.
proof: Proof. intros. assert (~ eq B A). { intro. assert (eq A B) by (conclude lemma_equalitysymmetric). contradict. } close. Qed.
imports: GeoCoq.Elements.OriginalProofs.lemma_equalitysymmetric