proposition: Lemma bet_inner_transitivity : ~ bet_inner_transitivityP Point Bet.
proof: Proof. unfold bet_inner_transitivityP, Bet. intro H; elim (H P0 P1 P2 P1); intuition discriminate. Qed.
imports: GeoCoq.Meta_theory.Counter_models.Planar.independence