proposition: Lemma inner_pasch : inner_paschP Point bet'.
proof: Proof. move=> a b c p q /andP[H00 H01] /andP[H10 H11] /eqP E1 /eqP E2 /eqP E3 /eqP E4. move: E1; rewrite -subr_eq0 vector2_neq0 !mxE !subr_eq0 => E1. move: E2; rewrite -subr_eq0 vector2_neq0 !mxE !subr_eq0 => E2. move: E3; rewrite -subr_eq0 vector2_neq0 !mxE !subr_eq0 => E3. move: E4; rewrite -subr_eq0 vector2_neq0 !mxE !subr_eq0 => E4. suffices: ((exists x0, bet (p 0 0)%:M x0 (b 0 0)%:M && bet (q 0 0)%:M x0 (a 0 0)%:M) /\ (exists x1, bet (p 0 1)%:M x1 (b 0 1)%:M && bet (q 0 1)%:M x1 (a 0 1)%:M)). move=> [[x0 /andP[Hx01 Hx02]] [x1 /andP[Hx11 Hx12]]]. exists (row2 (x0 0 0) (x1 0 0)); rewrite /bet' !mxE /= -2!mx11_scalar. by rewrite Hx01 Hx02 Hx11 Hx12. split; [move: H00 H10|move: H01 H11]; move: E1 E2 E3 E4. case: (a 0 0 =P p 0 0)=> [->|?]; [set x0 := p 0 0|case: (p 0 0 =P c 0 0)=> [->|?]; [set x0 := q 0 0|case: (b 0 0 =P q 0 0)=> [->|?]; [set x0 := q 0 0|case: (q 0 0 =P c 0 0)=> [->|?]; [set x0 := p 0 0|]]]]; try (exists (x0)%:M); rewrite ?bet_xxa ?bet_axx ?andbT /= 1?bet_sym ?H00 ?H10; rewrite //; move=> _ _ _ _ Hb1 Hb2; assert (H := @inner_pasch_gen R 1); destruct (H (a 0 0)%:M (b 0 0)%:M (c 0 0)%:M (p 0 0)%:M (q 0 0)%:M) as [x Hx]; try solve[move=> /matrixP /(_ 0 0) /eqP; rewrite !mxE !mulr1n=> /eqP E //]; [rewrite bet_sym Hb1|rewrite Hb2|exists x]=> //; by apply /andP. case: (a 0 1 =P p 0 1)=> [->|?]; [set x1 := p 0 1|case: (p 0 1 =P c 0 1)=> [->|?]; [set x1 := q 0 1|case: (b 0 1 =P q 0 1)=> [->|?]; [set x1 := q 0 1|case: (q 0 1 =P c 0 1)=> [->|?]; [set x1 := p 0 1|]]]]; try (exists (x1)%:M); rewrite ?bet_xxa ?bet_axx ?andbT /= 1?bet_sym ?H01 ?H11; rewrite //; move=> _ _ _ _ Hb1 Hb2; assert (H := @inner_pasch_gen R 1). destruct (H (a 0 1)%:M (b 0 1)%:M (c 0 1)%:M (p 0 1)%:M (q 0 1)%:M) as [x Hx]; try solve[move=> /matrixP /(_ 0 0) /eqP; rewrite !mxE !mulr1n=> /eqP E //]; [rewrite bet_sym Hb1|rewrite Hb2|exists x]=> //; by apply /andP. 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