proposition: Lemma big_nat_rev m n P F : \big[op/x]_(m <= i < n | P i) F i = \big[op/x]_(m <= i < n | P (m + n - i.+1)) F (m + n - i.+1).
proof: Proof. case: (ltnP m n) => ltmn; last by rewrite !big_geq. rewrite -{3 4}(subnK (ltnW ltmn)) addnA. do 2!rewrite (big_addn _ _ 0) big_mkord; rewrite (reindex_inj rev_ord_inj)/=. by apply: eq_big => [i | i _]; rewrite /= -addSn subnDr addnC addnBA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)