proposition: Lemma cong_pseudo_reflexivity : cong_pseudo_reflexivityP Point Cong.
proof: Proof. unfold cong_pseudo_reflexivityP, Cong; destruct A, B; intuition discriminate. Qed.
imports: GeoCoq.Meta_theory.Counter_models.Planar.independence