proposition: Lemma betweenC (a b c : Plane) : between a b c = between a c b.
proof: Proof. rewrite /between det_inverse -det_cyclique oppr_eq0; congr andb; rewrite !andbA; congr andb. by apply andbC. by rewrite eq_sym; apply implyb_id2l=>/eqP->. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise