proposition: Lemma in01M t u : in01 t -> in01 u -> in01 (t * u).
proof: Proof. move=>/andP[t0 t1]/andP[u0 u1]; apply/andP; split; first by apply mulr_ge0. by apply mulr_ile1. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise