proposition: Lemma prodBig1 : forall (n : nat) (x : nat -> nat), (forall z : nat, z < n -> x z > 0) -> prod n x > 0.
proof: Proof. induction n as [| n Hrecn]. - intros x H; simpl in |- *; apply Nat.lt_succ_diag_r. - intros x H; simpl in |- *; apply Nat.mul_pos_pos. + apply H; apply Nat.lt_succ_diag_r. + apply Hrecn; intros; now apply H, Nat.lt_lt_succ_r. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow