proposition: Lemma in01_convA t u : in01 t -> in01 u -> in01 (t / (1-(1-t)*(1-u))).
proof: Proof. move=> t01 u01. have c0 : 0 <= 1 - (1 - t) * (1 - u). by move:t01 u01; rewrite in01_onem=>t01; rewrite in01_onem=>/(in01M t01); rewrite in01_onem=>/andP[]. apply/andP; split. by apply divr_ge0=>//; move:t01=>/andP[]. have [->|e0] := eqVneq (1 - (1 - t) * (1 - u)) 0; first by rewrite invr0 mulr0; exact ler01. rewrite -{4}(divff e0). rewrite ler_wpmul2r ?invr_ge0//. rewrite mulrBr mulr1 mulrBl -addrA opprD addrA subrr add0r opprB opprK -mulrBl -subr_ge0 -addrA subrr addr0; apply mulr_ge0; last by move:u01=>/andP[]. by move:t01; rewrite in01_onem=>/andP[]. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise