proposition: Lemma itv_partition_nth_le a b s m : (m < (size s).+1)%N -> itv_partition a b s -> nth b (a :: s) m <= b.
proof: Proof. elim: m s a => [s a _|n ih]; first exact: itv_partition_le. by move=> [//|a h t /= nt] H; rewrite ih//; exact: itv_partition_cons H. 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)