proposition: Lemma between_depl (a b c : Plane) : between a b c <-> exists (d : Plane) (t u : R), (t*u <= 0) && (b == a + t *: d) && (c == a + u *: d).
proof: Proof. split. move=>/between_conv[t] /andP[t01]. have aconv: a = t *: a + (1-t) *: a by rewrite -scalerDl addrCA subrr addr0 scale1r. rewrite {1}aconv -subr_eq0 opprD addrACA -2!scalerBr. case t1: (t == 1). move:t1=>/eqP->; rewrite subrr scale1r scale0r addr0 subr_eq0=>/eqP->. exists (c-b), 0, 1. by rewrite mul0r lexx scale0r addr0 eqxx scale1r addrCA subrr addr0 eqxx. rewrite addr_eq0 -scalerN opprB=>/eqP e. exists (b-a), 1, (-t / (1-t)). move:t1=>/negbT; rewrite eq_sym -subr_eq0=>tn1. move:t01=>/andP[t0 t1]; rewrite mul1r mulNr oppr_le0 scale1r addrCA subrr addr0 eqxx mulrC scaleNr -scalerN opprB -scalerA e scalerA [_*(1-t)]mulrC divff// scale1r addrCA subrr addr0 eqxx 2!andbT; apply mulr_ge0=>//. by rewrite invr_ge0 subr_ge0. move=>[d][t][u]/andP[/andP[tu0]]. wlog: d t u tu0 / 0 < t. move=>h. have [t0|t0] := ltP 0 t; first by apply h. move:t0; rewrite le_eqVlt => /orP[|]. by move=>/eqP->; rewrite scale0r addr0=>/eqP-> _; apply betweenl. by rewrite -oppr_gt0 -(opprK d) 2![_ *: - - _]scalerN -2!scaleNr; apply h=>//; rewrite mulrN -mulNr opprK. move=>t0 /eqP be /eqP ce. move:tu0; rewrite pmulr_rle0// =>u0. have tugt0: 0 < t-u by rewrite subr_gt0; exact (le_lt_trans u0 t0). have tun0: t-u != 0 by apply/negP=>/eqP tu0; move:tugt0; rewrite tu0 ltxx. apply/between_conv; exists (-u/(t-u)); apply/andP; split. apply/andP; split. by rewrite mulr_ge0 ?oppr_ge0// invr_ge0 ltW. by rewrite -subr_ge0 -(pmulr_rge0 _ tugt0) mulrBr mulrCA divff// 2!mulr1 -addrA subrr addr0; apply ltW. by rewrite/conv be ce 2!scalerDr addrACA -scalerDl [_ + (1-_)]addrCA subrr addr0 scale1r -subr_eq0 opprD addrA subrr add0r oppr_eq0 2!scalerA -scalerDl mulrBl mul1r addrCA -mulrBr mulrAC -mulrA divff// mulr1 subrr scale0r. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise