proposition: Lemma notin_itv_partition c s : sorted <%R s -> c \notin s -> s = [seq x <- s | x < c] ++ itv_partitionR s c.
proof: Proof. elim: s c => // h t ih c /= ht. rewrite inE negb_or => /andP[]; rewrite neq_lt => /orP[ch|ch] ct. rewrite ch ltNge (ltW ch)/= path_lt_filter0/= /itv_partitionR; last first. exact: path_lt_head ht. by rewrite path_lt_filterT//; exact: path_lt_head ht. by rewrite ch/= ltNge (ltW ch)/= -ih//; exact: path_sorted ht. 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)