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