proposition: Lemma inner_pasch : inner_paschP Point bet'.
proof: Proof. move=> a b c p q /andP[Hb1 _] /andP[Hb2 _] ap_neq pc_neq bq_neq qc_neq HNC. destruct (inner_pasch Hb1 Hb2) as [x [Hb3 Hb4]]=> //. by move=> HC ; apply HNC, col_2D_bet', col_2D'. exists x; rewrite /bet' Hb3 Hb4 /=; case: (p =P x)=> /= [E|_]. exfalso; apply HNC, col_2D_bet'; rewrite -E in Hb4; suffices: (col' a b c)=> [//|]. apply bet_col' in Hb1; apply bet_col' in Hb2; apply bet_col' in Hb4. apply col_trans with q c=> //; rewrite col_perm_1 ?col_xxa // col_perm_1 //. by apply col_trans with a p=> //; rewrite col_perm_2 ?col_xxa // col_perm_1. case: (q =P x)=> /= [E|_ //]; exfalso; apply HNC, col_2D_bet'; rewrite -E in Hb3. suffices: (col' a b c)=> [//|]; apply bet_col' in Hb1; apply bet_col' in Hb2. apply bet_col' in Hb3; apply col_trans with p c=> //; rewrite col_perm_1; rewrite ?col_xxa // col_perm_1 //; apply col_trans with b q=> //; by rewrite col_perm_2 ?col_xxa // col_perm_1. 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.Axioms.gupta_inspired_variant_axioms GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence