proposition: Lemma conv_gt0 (a b : R^o) (t : {i01 R}) : 0 < a -> 0 < b -> 0 < a <| t |> b.
proof: Proof. move=> a0 b0. have [->|t0] := eqVneq t 0%:i01; first by rewrite conv0. have [->|t1] := eqVneq t 1%:i01; first by rewrite conv1. rewrite addr_gt0// mulr_gt0//; last by rewrite lt_neqAle eq_sym t0/=. by rewrite onem_gt0// lt_neqAle t1/=. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) mathcomp(functions cardinality) ereal reals signed topology prodnormedzmodule normedtype derive realfun itv HB(structures)