proposition: Theorem divProd2 : forall (n : nat) (x : nat -> nat) (i : nat), i <= n -> divide (prod i x) (prod n x).
proof: Proof. simple induction n. - intros x i ?; assert (H0: (0 = i)). { symmetry; now apply Nat.le_0_r. } rewrite H0. exists 1. lia. - intros n0 H x i H0. rewrite Nat.lt_eq_cases in H0; destruct H0. + simpl in |- *. rewrite Nat.mul_comm. assert (H2: i <= n0) by lia. destruct (H x i H2). rewrite H1. exists (x0 * x n0). lia. + rewrite H0; exists 1; lia. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow