proposition: Lemma itv_partition_nth_size def a b s : itv_partition a b s -> nth def (a :: s) (size s) = b.
proof: Proof. by elim: s a => [a/= /itv_partition_nil//|y t ih a /= /itv_partition_cons/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)