proposition: Lemma itv_partition_nth_ge a b s m : (m < (size s).+1)%N -> itv_partition a b s -> a <= nth b (a :: s) m.
proof: Proof. elim: m s a b => [s a b _//|n ih [//|h t] a b]. rewrite ltnS => nh [/= /andP[ah ht] lb]. by rewrite (le_trans (ltW ah))// ih. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)