proposition: Lemma big_rev_mkord m n P F : \big[op/x]_(m <= k < n | P k) F k = \big[op/x]_(k < n - m | P (n - k.+1)) F (n - k.+1).
proof: Proof. rewrite big_nat_rev (big_addn _ _ 0) big_mkord. by apply: eq_big => [i|i _]; rewrite -addSn addnC subnDr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)