proposition: Lemma variation_opp_rev a b f s : itv_partition a b s -> variation a b f s = variation (- b) (- a) (f \o -%R) (rev (belast (- a) (map -%R s))).
proof: Proof. move=> abl; rewrite belast_map /variation /= [LHS]big_nat_rev/= add0n. rewrite size_rev size_map size_belast 2!big_nat. apply: eq_bigr => k; rewrite leq0n /= => ks. rewrite nth_rev ?size_map ?size_belast// [in RHS]distrC. rewrite (nth_map a); last first. by rewrite size_belast ltn_subLR// addSn ltnS leq_addl. rewrite opprK -rev_rcons nth_rev ?size_rcons ?size_map ?size_belast 1?ltnW//. rewrite subSn// -map_rcons (nth_map b) ?size_rcons ?size_belast; last first. by rewrite ltnS ltn_subLR// addSn ltnS leq_addl. rewrite opprK nth_rcons size_belast -subSn// subSS. rewrite (ltn_subLR _ (ltnW ks)) if_same. case: k => [|k] in ks *. rewrite add0n ltnn subn1 (_ : nth b s _ = b); last first. case: abl ks => _. elim/last_ind : s => // h t _; rewrite last_rcons => /eqP -> _. by rewrite nth_rcons size_rcons ltnn eqxx. rewrite (_ : nth b (a :: s) _ = nth a (belast a s) (size s).-1)//. case: abl ks => _. elim/last_ind : s => // h t _; rewrite last_rcons => /eqP -> _. rewrite belast_rcons size_rcons/= -rcons_cons nth_rcons/= ltnS leqnn. exact: set_nth_default. rewrite addSn ltnS leq_addl//; congr (`| f _ - f _ |). elim/last_ind : s ks {abl} => // h t _; rewrite size_rcons ltnS => kh. rewrite belast_rcons nth_rcons subSS ltn_subLR//. by rewrite addSn ltnS leq_addl// subSn. elim/last_ind : s ks {abl} => // h t _; rewrite size_rcons ltnS => kh. rewrite belast_rcons subSS -rcons_cons nth_rcons /= ltn_subLR//. rewrite addnS ltnS leq_addl; apply: set_nth_default => //. by rewrite /= ltnS leq_subLR leq_addl. 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)