proposition: Lemma intersect_correct a b c d : intersect a b c d -> exists p, between p a b && between p c d.
proof: Proof. have sm t u : t *: (u : regular_lmodType R) = t * u by []. wlog abc0: a b c d / 0 <= det a b c. move=>h. case ge0: (0 <= det a b c); first by apply h. move:ge0=>/negP/negP; rewrite leNgt -oppr_gt0 -det_inverse -det_cyclique negbK intersectCl=>/ltW ge0 bacd. by move:(h _ _ _ _ ge0 bacd)=>[p]; rewrite betweenC=>pb; exists p. case ab: (a == b). by move=>/andP[/andP[/andP[_]]]; rewrite ab/==>acd _ _; exists a; rewrite betweenl. case cd: (c == d). by move=>/andP[_]/andP[/andP[_]]; rewrite cd/==>cab _; exists c; rewrite betweenl andbT. move=>/andP[/andP [/andP[absep _] ab0]] /andP[/andP[cdsep _] cd0]. move: abc0; rewrite le0r => /orP[|]. move=>/eqP/det0_aligned; case; first by move=>abe; move:ab; rewrite abe eqxx. move=>[t] ce; move: cdsep cd0; rewrite cd -ce 2!det_conv -![det _ d _]det_cyclique 2!det_alternate /conv 4!sm 2!mulr0 add0r addr0 det_inverse -det_cyclique mulrN mulNr mulrACA oppr_le0. case tlt: ((1-t) * t < 0). rewrite nmulr_rge0// -expr2=>badle. have-> : (det b a d = 0) by apply/eqP; rewrite -sqrf_eq0; apply/eqP/le_anti/andP; split=>//; apply sqr_ge0. rewrite 2!mulr0 oppr0 eqxx/= =>/or3P[| |]; last first. by move=>/andP[acd _]; exists a; rewrite betweenl. by exists d; rewrite betweenr andbT. by move=> cdb; exists (a <| t |> b); rewrite betweenl andbT. move=>_ _; exists (a <| t |> b); rewrite betweenl andbT; apply between_conv. by exists t; rewrite eqxx andbT in01M_ge0 leNgt mulrC tlt. move:ab0=> _ abc; move:absep; rewrite pmulr_rle0// =>abd. set t := det a b d / (det d a b - det c a b). have denom: det d a b - det c a b != 0 by rewrite 2![det _ a b]det_cyclique subr_eq0; apply/negP=>/eqP detE; move:(le_lt_trans abd abc); rewrite detE ltxx. have: det a b (c <| t |> d) == 0 by rewrite -det_cyclique det_conv convrl sm -opprB mulrN /t -mulrA [_^-1 * _]mulrC divff// mulr1 det_cyclique subrr. move=>/eqP /det0_aligned; case; first by move=>/eqP; rewrite ab. move=>[u utE]. case u01: (in01 u). exists (a <| u |> b); apply/andP; split. apply between_conv. by exists u; rewrite u01 eqxx. rewrite utE; apply between_conv. exists t; rewrite eqxx andbT in01M_ge0 -(divff denom) /t -mulrBl mulrACA addrAC ![det _ a b]det_cyclique subrr add0r mulrN -mulNr -expr2; apply mulr_ge0; last first. by apply sqr_ge0. by apply mulr_ge0; [ rewrite oppr_ge0 | apply ltW ]. move:u01; rewrite in01M_ge0 leNgt=>/negbT; rewrite negbK=>u01. move:(u01); rewrite -oppr_gt0 lt0r oppr_eq0 mulf_eq0 negb_or=>/andP[/andP [/lregP u0 /lregP u1] _]. have: det (a <| u |> b) c d == 0 by rewrite utE det_conv -[det d _ _]det_cyclique 2!det_alternate convmm. rewrite det_conv 2![det _ c d]det_cyclique addr_eq0 2!sm=>/eqP udetE. move:cdsep; rewrite -(nmulr_rge0 _ u01) mulrACA udetE mulNr oppr_ge0 -expr2=>det2_le0. have /eqP cdb0: det c d b == 0 by rewrite -(mulrI_eq0 _ u1) -sqrf_eq0; apply/eqP/le_anti/andP; split=>//; apply sqr_ge0. move:udetE=>/eqP; rewrite cdb0 mulr0 oppr0 mulrI_eq0// =>/eqP cda0. move:cd0; rewrite cdb0 cda0 eqxx cd/= =>/or3P[cab|dab|]; last first. - by move=>/andP[acd _]; exists a; rewrite betweenl. - by exists d; rewrite betweenr andbT. - by exists c; rewrite betweenl andbT. Qed.
imports: counterclockwise conv encompass preliminaries mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets constructive_ereal) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)