proposition: Lemma dup_meet a b c d : uniq [:: a; b; c; d] = false -> exists y, Col (Point R) (@bet' R) a b y /\ Col (Point R) (@bet' R) c d y.
proof: Proof. move=> H; have: (~~ uniq [:: a; b; c; d]) by rewrite H. move: H=> _ H. move/uniqPn: H=> H; move: H (H a)=> _ [i [j [H1 H2 H3]]]; move: H1 H2 H3. case: j; rewrite ?ltn0 //= => j; repeat try (case: j=> [|j //=]); repeat try (case: i=> [|i //=])=> /=; move=> _ _ ->; try solve [exists b; split; rewrite /Col /bet' ?bet_axx ?bet_xxa; intuition]; try solve [exists c; split; rewrite /Col /bet' ?bet_axx ?bet_xxa; intuition]; exists d; split; rewrite /Col /bet' ?bet_axx ?bet_xxa; intuition. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype choice seq) mathcomp(fintype finset finfun bigop order) mathcomp(ssralg ssrnum path generic_quotient matrix mxalgebra) mathcomp(zmodp) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence