proposition: Lemma in01M1 t u : in01 t -> in01 u -> (t * u == 1) = (t == 1) && (u == 1).
proof: Proof. move=>/andP[t0 t1]/andP[u0 u1]. apply/idP/idP; last by move=>/andP[/eqP-> /eqP->]; rewrite mulr1. case tn1: (t == 1); first by move:tn1=>/eqP->; rewrite mul1r. case un1: (u == 1); first by move:un1=>/eqP->; rewrite mulr1 tn1. move=>/eqP tu1/=. suff: t * u < 1 by rewrite tu1 ltxx. by apply mulr_ilt1=>//; rewrite -subr_gt0 lt0r subr_eq0 subr_ge0 eq_sym ?t1 ?u1 ?tn1 ?un1. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise