proposition: Lemma Nfinite_prod_index_reversal : forall n f, Nfinite_prod_0_n n f = Nfinite_prod_0_n n (fun k => f(n - k)).
proof: Proof. induction n. compute. reflexivity. intros. rewrite Nfinite_prod_split_upper. rewrite Nfinite_prod_split_lower. rewrite IHn. rewrite Nat.sub_0_r. assert (Nfinite_prod_0_n n (fun k : nat => f (S n - S k)) = Nfinite_prod_0_n n (fun k : nat => f (n - k))). apply Nfinite_prod_subtle_eq_compat. intros. assert (S n-S k=n-k). auto with arith. rewrite H0. reflexivity. rewrite H. ring. Qed.
imports: Arith Compare Nk_ind Npow Ndiv