proposition: Lemma all_lines_meet a b c d : exists y, Col (Point R) (@bet' R) a b y /\ Col (Point R) (@bet' R) c d y.
proof: Proof. move: (permP a b c d)=> [e [f [g [h /and4P[H H1 H2 /and4P[H3 H4 H5 H6]]]]]]. move: H (perm_mem H) (perm_uniq H)=> _ H; move: H (H a) (H b) (H c) (H d). move: (line_intersection_1 H1 H2 H3 H4 H5 H6)=> [y1 [Y11 Y12]]. move: (line_intersection_2 H1 H2 H3 H4 H5 H6)=> [y2 [Y21 Y22]]. move: (line_intersection_3 H1 H2 H3 H4 H5 H6)=> [y3 [Y31 Y32]]. move=> _ aP bP cP dP; move: H1 H2 H3 H4 H5 H6=> _ _ _ _ _ _. case (uniq [:: e; f; g; h] =P true)=> [H|]; rewrite ?H; last by rewrite Bool.not_true_iff_false => ->; apply dup_meet. move=> H1; have: (uniq [:: a; b; c; d] = uniq [:: e; f; g; h]) by rewrite H H1. move=> H2; move: Y22 (col_213 Y22) Y31 (col_213 Y31) Y32 (col_213 Y32). move: H2 H H1 aP bP cP dP Y11 (col_213 Y11) Y12 (col_213 Y12) Y21 (col_213 Y21). rewrite /uniq !in_cons !eqxx !orbT /= !in_nil=> uniqP. case: (e =P f)=> [-> //=|]; case: (e =P g)=> [-> //=|]. case: (e =P h)=> [-> //=|]; case: (f =P g)=> [-> //=|]. case: (f =P h)=> [-> //=|]; case: (g =P h)=> [-> //=|/=]; move: uniqP. case: (a =P b)=> [-> //=|]; case: (a =P c)=> [-> //=|]. case: (a =P d)=> [-> //=|]; case: (b =P c)=> [-> //=|]. case: (b =P d)=> [-> //=|]; case: (c =P d)=> [-> //=|/=]. move=> H1 H2 H3 H4 H5 H6 uniqP; move: uniqP H1 H2 H3 H4 H5 H6. case: (a =P e)=> [ae_eq|_]; case: (a =P f)=> [af_eq|_]; case: (a =P g)=> [ag_eq|_]; case: (a =P h)=> [ah_eq|_]; rewrite -?ae_eq -?af_eq -?ag_eq -?ah_eq // ?ae_eq ?af_eq ?ag_eq ?ah_eq; case: (b =P e)=> [be_eq|_]; case: (b =P f)=> [bf_eq|_]; case: (b =P g)=> [bg_eq|_]; case: (b =P h)=> [bh_eq|_]; rewrite -?be_eq -?bf_eq -?bg_eq -?bh_eq // ?be_eq ?bf_eq ?bg_eq ?bh_eq; case: (c =P e)=> [ce_eq|_]; case: (c =P f)=> [cf_eq|_]; case: (c =P g)=> [cg_eq|_]; case: (c =P h)=> [ch_eq|_]; rewrite -?ce_eq -?cf_eq -?cg_eq -?ch_eq // ?ce_eq ?cf_eq ?cg_eq ?ch_eq; case: (d =P e)=> [de_eq|_]; case: (d =P f)=> [df_eq|_]; case: (d =P g)=> [dg_eq|_]; case: (d =P h)=> [dh_eq|_]; rewrite -?de_eq -?df_eq -?dg_eq -?dh_eq // ?de_eq ?df_eq ?dg_eq ?dh_eq; move=> _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _; move=> Y11 Y11' Y12 Y12' Y21 Y21' Y22 Y22' Y31 Y31' Y32 Y32'; try solve [exists y1; split; rewrite ?Y11 ?Y11' ?Y12 ?Y12'=> //]; try solve [exists y2; split; rewrite ?Y21 ?Y21' ?Y22 ?Y22'=> //]; by exists y3; split; rewrite ?Y31 ?Y31' ?Y32 ?Y32'. 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