proposition: Lemma betweenl (a b : Plane) : between a a b.
proof: Proof. rewrite/between det_alternate eqxx/= subrr -(scale0r 0) scalar_productZL mul0r lexx/= Bool.implb_same andbT; apply scalar_productrr_ge0. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise