proposition: Lemma big_ord_rev (n : nat) (P : nat -> bool) (F : nat -> R): \big[op/idx]_(i < n | P i) F i = \big[op/idx]_(i < n | P (n - i.+1)%N) F ( n - i.+1)%N.
proof: Proof. by rewrite - big_mkord big_nat_rev add0n big_mkord. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)