proposition: Lemma in01_convl (t u : R) : 0 <= t*u -> in01 (t / (t+u)).
proof: Proof. have H: forall a b : R, 0 <= a*b -> 0 <= a/(a+b) by move=>a b ab0; rewrite -sgr_ge0 sgrM sgrV -sgrM sgr_ge0 mulrDr -expr2; apply addr_ge0=>//; apply sqr_ge0. move=>tu0. have [->|tun0] := eqVneq (t + u) 0. by rewrite invr0 mulr0; apply in010. apply/andP; split; first by apply H. rewrite -{1}[t](addr0) -(subrr u) addrA mulrBl divff// -subr_ge0 opprB addrCA subrr addr0 addrC; apply H. by rewrite mulrC. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise