proposition: Lemma divProd : forall (n : nat) (x : nat -> nat) (i : nat), i < n -> divide (x i) (prod n x).
proof: Proof. induction n as [| n Hrecn]. - intros x i H; destruct (Nat.nlt_0_r _ H). - intros x i H. assert (lein: i <= n) by lia; rewrite Nat.lt_eq_cases in lein; destruct lein. + simpl in |- *. rewrite Nat.mul_comm. destruct (Hrecn x i H0). rewrite H1. exists (x0 * x n). lia. + subst. simpl. exists (prod n x). auto. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow