proposition: Lemma bet_inner_transitivity : bet_inner_transitivityP Point Bet.
proof: Proof. unfold bet_inner_transitivityP, Bet; destruct A, B, C, D; intuition discriminate. Qed.
imports: GeoCoq.Meta_theory.Counter_models.Planar.independence