proposition: Lemma intersect_complete a b c d : (exists p, between p a b && between p c d) -> intersect a b c d.
proof: Proof. have sm: forall t u, t *: (u : regular_lmodType R) = t*u by []. move:a b c d. suff: forall a b c d, (exists p : counterclockwise.Plane R, between p a b && between p c d) -> separate a b c d. move=> h a b c d abcd; apply/andP; split; apply h=>//. by move:abcd=>[p]; rewrite andbC=>pabcd; exists p. move=>a b c d [p] /andP[/between_conv] [t] /andP[t01] /eqP pe /between_conv [u] /andP[u01] /eqP pe'; subst p; rewrite/separate -andbA. apply/andP; split. have: det (a <| t |> b) a b == 0 by rewrite det_conv -[det b a b]det_cyclique 2!det_alternate convmm. rewrite pe' det_conv 2![det _ a b]det_cyclique addr_eq0 2!sm=>/eqP detE. move:u01; rewrite in01M_ge0 le0r =>/orP[|]. rewrite mulf_eq0 subr_eq0 => /orP[|] /eqP ue; move:detE=>/eqP. by rewrite ue mul0r subr0 mul1r eq_sym oppr_eq0=>/eqP->; rewrite mulr0. by rewrite -ue mul1r subrr mul0r oppr0=>/eqP->; rewrite mul0r. by move=>ui; rewrite -(pmulr_rle0 _ ui) mulrACA detE mulNr oppr_le0 -expr2; apply sqr_ge0. case ab : (a == b)=>/=. by move: ab=>/eqP ab; subst b; rewrite 2!det_alternate eqxx/= andbT; apply between_conv; exists u; apply/andP; split=>//; rewrite -pe' convmm. apply/implyP=>/eqP/det0_aligned[]; first by move=>/eqP; rewrite ab. move=>[t'] ce; apply/implyP=> /eqP/det0_aligned[]; first by move=>/eqP; rewrite ab. move=>[u'] de. wlog: c d u t' u' pe' u01 ce de / t' <= u'. move=>h. case tu: (t' <= u'); first by apply (h c d u t' u'). move:tu; rewrite leNgt=>/negbT; rewrite negbK=>/ltW ut. by rewrite 2![_ _ c d]betweenC andbC; apply (h d c (1-u) u' t')=>//; rewrite -?in01_onem -?convC. move=>tu. move:pe'; rewrite -{1}ce -{1}de /conv 3![(_ - _) *: b]scalerBl scale1r 3![_ *: _ + (_ - _)]addrCA -3!scalerBr 2![_ *: (_ + _ *: _)]scalerDr addrACA -scalerDl [u+(1-u)]addrCA subrr addr0 scale1r 2!scalerA -scalerDl=>/addrI/eqP. rewrite -subr_eq0 -scalerBl scaler_eq0 2!subr_eq0 ab orbF=>tconv. case t0: (t' < 0). apply/or3P/Or32. apply/between_depl; exists (a-b), t', u'; rewrite -ce -de 2!convrl 2!eqxx 2!andbT nmulr_rle0//. move:u01 tconv=>/andP[u0]; rewrite -[u<=1]subr_ge0 le0r subr_eq0 -invr_gt0 => /orP[|]. by move=>/eqP<-; rewrite subrr mul1r mul0r addr0=>/eqP te; move:t01=>/andP[]; rewrite te leNgt t0. move=>ugt0. have un0: (1-u)^-1 != 0 by apply/negP=>/eqP ue; move:ugt0; rewrite ue ltxx. move:un0 (un0); rewrite {1}invr_eq0=>un0 /rregP ureg. rewrite -subr_eq0 -(mulIr_eq0 _ ureg) opprD addrA mulrBl mulrAC divff// mul1r subr_eq0=>/eqP<-; apply mulr_ge0; last by apply ltW. apply addr_ge0; first by move:t01=>/andP[t0' _]. by rewrite -mulrN mulr_ge0 // oppr_ge0 ltW. move:t0=>/negbT; rewrite -leNgt=>t0. case u1: (1 < u'). apply/or3P/Or31. apply/between_depl; exists (b - a), (1 - t'), (1 - u'); rewrite -2!convlr ce de 2!eqxx 2!andbT. move:u01 tconv=>/andP; rewrite le0r=>[[/orP[|]]]. move=>/eqP-> _; rewrite subr0 mul0r mul1r add0r=>/eqP tu'. by move:t01; rewrite tu'=>/andP[_]/(lt_le_trans u1); rewrite ltxx. move:u1; rewrite -subr_lt0=>ugt1 u0 u1; rewrite nmulr_lle0//. have un0 : u != 0 by rewrite gt_eqF. move:(un0); rewrite -invr_eq0=>/rregP ureg. rewrite -subr_eq0 -(mulIr_eq0 _ ureg) opprD addrCA addrC mulrBl mulrAC divff// mul1r subr_eq0=>/eqP<-; rewrite -(pmulr_rge0 _ u0) mulrBr mulrCA divff// 2!mulr1 opprB addrA subr_ge0. move:t01=>/andP[_] t1. apply (le_trans t1); rewrite -subr_ge0 addrAC -opprB -mulrN1 -mulrDr [-1+_]addrC. by rewrite mulr_ge0// subr_ge0// -subr_le0 ltW. move:u1=>/negbT; rewrite -leNgt=>u1. apply/or3P/Or33. apply/andP; split; apply between_conv. by exists t'; rewrite ce eqxx andbT /in01 t0/= (le_trans tu). by exists u'; rewrite de eqxx andbT /in01 u1 (le_trans t0). 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)