proposition: Lemma in01_onem t : in01 t = in01 (1 - t).
proof: Proof. by rewrite 2!in01M_ge0 opprB addrCA subrr addr0 mulrC. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise