proposition: Lemma in01M_ge0 (t : R) : in01 t = (0 <= t * (1-t)).
proof: Proof. apply/idP/idP. by move=>/andP[t0 t1]; apply mulr_ge0=>//; rewrite subr_ge0. move=>ge0; apply/andP; split; rewrite leNgt; apply/negP=>ti; move:ge0. by rewrite nmulr_rge0// subr_le0=>t1; move:(lt_trans ltr01 (le_lt_trans t1 ti)); rewrite ltxx. by move:(ti); rewrite -subr_lt0=>t1'; rewrite nmulr_lge0// =>t0; move:(lt_trans (le_lt_trans t0 ltr01) ti); rewrite ltxx. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise