proposition: Lemma line_intersection_1 a b c d : (a 0 0 <= b 0 0) -> (c 0 0 <= d 0 0) -> (c 0 1 <= a 0 1) -> (d 0 1 <= a 0 1) -> (c 0 1 <= b 0 1) -> (d 0 1 <= b 0 1) -> exists y, Col (Point R) (@bet' R) a d y /\ Col (Point R) (@bet' R) b c y.
proof: Proof. move=> ab_le0 cd_le0 ca_le1 da_le1 cb_le1 db_le1. have: (bet (d 0 1)%:M (Num.min (a 0 1) (b 0 1))%:M (a 0 1)%:M)=> [|betPy1]. case: (a 0 1 =P b 0 1)=> [->|/eqP H]; first by rewrite minxx bet_axx. move: (lt_total H)=> /orP[?|?]; [rewrite min_l|rewrite min_r]; by rewrite ?ltW // ?bet_axx // bet_1Di ?lexx // ltW. have: (bet (c 0 1)%:M (Num.min (a 0 1) (b 0 1))%:M (b 0 1)%:M)=> [|betPy2]. case: (a 0 1 =P b 0 1)=> [->|/eqP H]; first by rewrite minxx bet_axx. move: (lt_total H)=> /orP[?|?]; [rewrite min_l|rewrite min_r]; by rewrite ?ltW // bet_1Di ?lexx // ltW. exists (row2 (Num.max (a 0 0) (c 0 0)) (Num.min (a 0 1) (b 0 1))). split; right; left; rewrite /bet' !mxE /= ?betPy1 ?betPy2 andbT. case: (a 0 0 =P c 0 0)=> [->|/eqP H]; first by rewrite max_l ?bet_1Dd ?lexx. move: (lt_total H)=> /orP[?|?]; [rewrite max_r|rewrite max_l]; by rewrite ?ltW // ?bet_axx // bet_1Dd ?lexx // ltW. case: (a 0 0 =P c 0 0)=> [->|/eqP H]; first by rewrite max_l ?bet_xxa ?lexx. move: (lt_total H)=> /orP[?|?]; [rewrite max_r|rewrite max_l]; by rewrite ?ltW // ?bet_xxa // bet_1Di ?lexx // ltW. 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