proposition: Lemma itv_partition_size_neq0 a b s : (size s > 0)%N -> itv_partition a b s -> a < b.
proof: Proof. elim: s a => // x [_ a _|h t ih a _]; rewrite /itv_partition /=. by rewrite andbT => -[ax /eqP <-]. move=> [] /andP[ax /andP[xy] ht /eqP tb]. by rewrite (lt_trans ax)// ih// /itv_partition /= xy/= tb. 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)