proposition: Lemma betweenr (a b : Plane) : between a b a.
proof: Proof. rewrite betweenC; apply betweenl. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise