proposition: Lemma prodExtensional : forall (n : nat) (x1 x2 : nat -> nat), (forall z : nat, z < n -> x1 z = x2 z) -> prod n x1 = prod n x2.
proof: Proof. induction n as [| n Hrecn]. - intros; reflexivity. - intros x1 x2 H; simpl in |- *; replace (x1 n) with (x2 n). + f_equal; auto. + rewrite (H n); auto. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow