proposition: Lemma between_conv x y z : between x y z <-> exists t, in01 t && (x == y <| t |> z).
proof: Proof. case yz: (y == z). rewrite/between yz; move:yz=>/eqP yz; rewrite yz subrr -(scale0r 0) scalar_productZR mul0r det_cyclique det_alternate eqxx lexx/=. split; first by move=>/eqP->; exists 0; rewrite in010 convmm/=. by move=>[t /andP[_]]; rewrite convmm. rewrite /between yz/= andbT. move:yz=>/negbT yz. have zye: forall t (y z: Plane), t *: y + (1-t) *: z - y = (1-t) *: (z-y). by move=>t y' z'; rewrite {1}[_*:_+_]addrC -addrA scalerBr; congr +%R; rewrite -scaleNr opprB scalerBl scale1r. have yze: forall t (y z: Plane), t *: y + (1-t) *: z - z = t *: (y-z). by move=>t y' z'; rewrite -addrA scalerBr; congr +%R; rewrite scalerBl scale1r [_-_*:_]addrC -addrA subrr addr0. split. rewrite det_cyclique =>/and3P[/eqP/det0_aligned]; case; first by move=> yz'; move:yz' yz=>->; rewrite eqxx. move=>[t <-]. rewrite yze zye 2!scalar_productZL=> yp zp; exists t; apply/andP; split=>//. apply/andP; split. by move:zp; rewrite pmulr_lge0//; apply scalar_productrr_gt0; rewrite subr_eq0. by move:yp; rewrite pmulr_lge0 ?subr_ge0//; apply scalar_productrr_gt0; rewrite subr_eq0 eq_sym. move=>[t] /andP [/andP [t0 t1]] /eqP->. rewrite yze zye 2!scalar_productZL; apply/and3P; split. - by rewrite det_cyclique; apply/eqP; apply det0_aligned; right; exists t. - by rewrite mulr_ge0// ?subr_ge0// scalar_productrr_ge0. - by rewrite mulr_ge0// scalar_productrr_ge0. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise