proposition: Lemma itv_partitionLP a b c s : a < c -> c < b -> itv_partition a b s -> itv_partition a c (itv_partitionL s c).
proof: Proof. move=> ac bc [] al /eqP htb; split. rewrite /itv_partitionL rcons_path/=; apply/andP; split. by apply: path_filter => //; exact: lt_trans. exact: (last_filterP [pred x | x < c]). by rewrite /itv_partitionL last_rcons. 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)