proposition: Lemma itv_partitionRP a b c s : a < c -> c < b -> itv_partition a b s -> itv_partition c b (itv_partitionR s c).
proof: Proof. move=> ac cb [] sa /eqP alb; rewrite /itv_partition; split. move: sa; rewrite lt_path_sortedE => /andP[allas ss]. rewrite lt_path_sortedE filter_all/=. by apply: sorted_filter => //; exact: lt_trans. exact/eqP/(path_lt_last_filter ac). 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)