(* 4^n + 15 n - 1 % 9 *) Require Import Arith. Require Import ZArith. Open Scope Z_scope. Require Import Lia. Fixpoint pow (a : Z) (n : nat) : Z := match n with | 0%nat => 1%Z | S k => (pow a k) * a end. Fixpoint ntoz (n : nat) : Z := match n with | 0%nat => 0%Z | S k => (ntoz k) + 1 end. Theorem z7 : forall n : nat, exists q : Z, pow 4 n + 15 * (ntoz n) - 1 = 9 * q. Proof. intros. induction n. exists 0. auto with zarith. elim IHn. intros. simpl (pow 4 (S n)). simpl (ntoz (S n)). assert (pow 4 n = 9*x - 15*ntoz n + 1). auto with zarith. rewrite H0. ring_simplify ((9 * x - 15 * ntoz n + 1) * 4 + 15 * (ntoz n + 1) - 1). exists (4*x-5*ntoz n+2). ring. Qed. Theorem z8 : forall n : nat, exists q : Z, pow 11 (n + 2)%nat + pow 12 ((2 * n)%nat + 1)%nat = 133 * q. Proof. induction n. simpl ((pow 11 (0 + 2))). simpl ((pow 12 (2*0 + 1))). exists 1. auto with zarith. simpl (pow 11 (S n + 2)). assert ((2 * S n + 1)%nat = S (S (2*n+1))). ring. rewrite H. simpl (pow 12 (S (S (2 * n + 1)))). elim IHn. intros. assert (pow 11 (n+2) = 133*x - pow 12 (2 * n + 1)). auto with zarith. rewrite H1. assert ((n + (n + 0) + 1)%nat = (2 * n + 1)%nat). ring. rewrite H2. ring_simplify ((133 * x - pow 12 (2 * n + 1)) * 11 + pow 12 (2 * n + 1) * 12 * 12). exists (11*x + pow 12 (2 * n + 1)). ring. Qed. Fixpoint sum (a : nat -> Z) (n : nat) := match n with | 0%nat => 0 | S m => (sum a m) + (a m) end. (* sum a n = a_0 + a_1 + ... + a_{n-1} *) (* m = n-1 *) Theorem z10 : forall m : nat, forall a b : (nat -> Z), sum (fun k:nat => (a k) * (b k)) (S m) = sum (fun k:nat => (sum a (S k)) * (b k - b (S k))) m + (sum a (S m)) * b m. Proof. intros. induction m. simpl. reflexivity. simpl. simpl in IHm. rewrite IHm. ring_simplify. ring. Qed.