proposition: Lemma in_itv_partition c s : sorted <%R s -> c \in s -> s = itv_partitionL s c ++ itv_partitionR s c.
proof: Proof. elim: s c => // h t ih c /= ht. rewrite inE => /predU1P[->{c}/=|ct]. rewrite ltxx /itv_partitionL /= ltxx /itv_partitionR/= path_lt_filter0//=. by rewrite path_lt_filterT. rewrite /itv_partitionL/=; case: ifPn => [hc|]. by rewrite ltNge (ltW hc)/= /= [in LHS](ih _ _ ct)//; exact: path_sorted ht. rewrite -leNgt le_eqVlt => /predU1P[ch|ch]. by rewrite ch ltxx path_lt_filter0//= /itv_partitionR path_lt_filterT. move: ht; rewrite lt_path_sortedE => /andP[/allP/(_ _ ct)]. by move=> /lt_trans-/(_ _ ch); rewrite ltxx. 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)