proposition: Lemma between_trans (a b c d e : Plane) : between c a b -> between d a b -> between e c d -> between e a b.
proof: Proof. move=>/between_conv[t]/andP[t01 /eqP->] /between_conv[u]/andP[u01 /eqP->] /between_conv[v]/andP[v01 /eqP->]. rewrite convACA// 2!convmm. apply between_conv; exists ((t : R^o) <| v |> u); apply/andP; split=>//. by apply in01_conv. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise