proposition: Lemma cong_inner_transitivity : ~ cong_inner_transitivityP Point Cong.
proof: Proof. unfold cong_inner_transitivityP, Cong; intro H. elim (H P0 P1 P2 P2 P1 P0); try tauto; [intro HF|intros [H1 H2]]; discriminate. Qed.
imports: GeoCoq.Meta_theory.Counter_models.Planar.independence