proposition: Lemma itv_partition_rev a b s : itv_partition a b s -> itv_partition (- b) (- a) (rev (belast (- a) (map -%R s))).
proof: Proof. move=> [sa /eqP alb]; split. rewrite (_ : - b = last (- a) (map -%R s)); last by rewrite last_map alb. rewrite rev_path// path_map. by apply: sub_path sa => x y xy/=; rewrite ltrNr opprK. case: s sa alb => [_ <-//|h t] /= /andP[ah ht] <-{b}. by rewrite rev_cons 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)