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_rev_mkord subn0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)