proposition: Lemma permP a b c d : exists e f g h : Point R, [&& perm_eq [:: a; b; c; d] [:: e; f; g; h], (e 0 0 <= f 0 0), (g 0 0 <= h 0 0) & [&& (g 0 1 <= e 0 1), (h 0 1 <= e 0 1), (g 0 1 <= f 0 1) & (h 0 1 <= f 0 1)]].
proof: Proof. move: (perm_sort (fun p q : (@Point R) => q 0 1 <= p 0 1) [:: a; b; c; d]). have: (total (fun p q : (@Point R) => q 0 1 <= p 0 1))=> [p q|totalP]. case: (p 0 1 =P q 0 1)=> [->|/eqP H]; rewrite ?lexx //. by move: (lt_total H)=> /orP[HLt|HLt]; rewrite (ltW HLt) ?orbT. pose s := (sort (fun p q : Point R => q 0 1 <= p 0 1) [:: a; b; c; d]). move: totalP (sort_sorted totalP [:: a; b; c; d]); rewrite -/s=> _ seqP1 seqP2. have: (exists e f g h, s = [:: e; f; g; h])=> [|[e [f [g [h sP]]]]]. exists (nth a s 0), (nth a s 1), (nth a s 2), (nth a s 3). move: (size_sort (fun p q : Point R => q 0 1 <= p 0 1) [:: a; b; c; d]). rewrite -/s=> Hsize; apply eq_from_nth with a; first by move: Hsize. rewrite Hsize; move=> i; case i=> //=; repeat (move=> n; case: n => //=). move: seqP1; rewrite sP=> /= /and4P[HLe1 HLe2 HLe3 _]. suff: ([:: e; f; g; h] = [:: e; f] ++ [:: g; h])=> [Eq1|//=]. suff: ([:: f; e; g; h] = [:: f; e] ++ [:: g; h])=> [Eq2|//=]. suff: ([:: e; f; h; g] = [:: e; f] ++ [:: h; g])=> [Eq3|//=]. suff: ([:: f; e; h; g] = [:: f; e] ++ [:: h; g])=> [Eq4|//=]. suff: ([:: f; e] = rcons [:: f] e)=> [Eq5|//=]. suff: ([:: h; g] = rcons [:: h] g)=> [Eq6|//=]. case: (e 0 0 =P f 0 0)=> [ef_eq|/eqP H]; [|move: H (lt_total H)=> _]. case: (g 0 0 =P h 0 0)=> [gh_eq|/eqP H]; [|move: H (lt_total H)=> _]. exists e, f, g, h; rewrite -ef_eq -gh_eq !lexx -sP perm_sym permEl //. by rewrite !(le_trans HLe3) ?(le_trans HLe2) ?lexx. move=> /orP[HLt|HLt]; [exists e, f, g, h|exists e, f, h, g]; rewrite !(le_trans HLe3) ?(le_trans HLe2) ?lexx // -ef_eq lexx (ltW HLt); rewrite !andbT; apply perm_trans with s; rewrite perm_sym; rewrite sP ?perm_refl //; try solve [rewrite -sP permEl //]. by rewrite Eq1 Eq3 Eq6 perm_cat2l perm_rcons perm_refl. case: (g 0 0 =P h 0 0)=> [gh_eq|/eqP H]; [|move: H (lt_total H)=> _]. move=> /orP[HLt|HLt]; [exists e, f, g, h|exists f, e, g, h]; rewrite !(le_trans HLe3) ?(le_trans HLe2) ?lexx // -gh_eq lexx (ltW HLt); rewrite !andbT; apply perm_trans with s; rewrite perm_sym; rewrite sP ?perm_eq_refl //; try solve [rewrite -sP permEl //]. by rewrite Eq1 Eq2 Eq5 perm_cat2r perm_rcons perm_refl. move=> /orP[HLt1|HLt1] /orP[HLt2|HLt2]; [exists e, f, g, h|exists f, e, g, h|exists e, f, h, g|exists f, e, h, g]; rewrite !(le_trans HLe3) ?(le_trans HLe2) ?lexx // (ltW HLt1) (ltW HLt2); rewrite !andbT; apply perm_trans with s; rewrite perm_sym; rewrite sP ?perm_refl //; try solve [rewrite -sP permEl //]; [| |apply perm_trans with ([:: e; f; h; g])]; rewrite ?Eq1 ?Eq2 ?Eq3 ?Eq4; by rewrite ?Eq5 ?Eq6 ?perm_cat2l ?perm_cat2r ?perm_rcons perm_refl. 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