proposition: Lemma point_equality_decidability : point_equality_decidability Point.
proof: Proof. unfold point_equality_decidability; destruct A, B; try tauto; right; discriminate. Qed.
imports: GeoCoq.Meta_theory.Counter_models.Planar.independence