Require Export ArithRing.
Require Export Arith.
Inductive even : nat -> Prop :=
even0 : even 0
| evenS : forall x:nat, even x -> even (S (S x)).

Theorem even_mult : forall x, even x -> exists y, x = 2*y.
Proof.
intros x H.
elim H.
exists 0.
ring.
intros x0 Hevenx0 IHx.

destruct IHx as [y Heq].
rewrite Heq.
exists (S y).
ring.
Qed.

Fixpoint sum_n (n:nat) : nat :=
match n with 0 => 0 | S p => S p + sum_n p end.

Definition f1 n m := sum_n (n+m).
Definition f2 n m := sum_n n +sum_n m +m*n.
(* Eval compute in f1 3 0.
Eval compute in f2 3 0.*)

Lemma sum_n_sum:forall n m, sum_n (n+m)=sum_n n +sum_n m +m*n.
Proof.
induction n.
simpl.
intros;ring.

simpl.
intros.
rewrite (IHn m).
generalize (sum_n n);intros.
generalize sum_n m;intros.
ring.
Qed.

Theorem clasico: forall n:nat, 2 * sum_n n = n*n + n.
Proof.
induction n.
simpl.
trivial.
simpl.
assert (n + sum_n n + S (n + sum_n n + 0) = S(2*n + 2*sum_n n)).
generalize (sum_n n).
intros;ring.
rewrite H.
rewrite IHn.
ring.
Qed.

Fixpoint nat_power (b:nat) (e:nat) {struct e}: nat:=
match e with
  0 => 1
| (S x) => (nat_power b x)*b
end.

Infix "^" := nat_power (at level 30, right associativity).

(*Algunas propiedades*)
Lemma uno:forall n, 1^n=1.
Proof.
induction n;simpl;auto.
rewrite IHn.
auto.
Qed.

Lemma precrec:forall a b c, a<=b -> a*c <= b*(S c).
Proof.
intros a b c Hord.
assert (a*c <= b*c).
apply mult_le_compat_r.
auto.
assert (b*c <= b*(S c)).
apply mult_le_compat_l.
auto with arith.
apply le_trans with (b*c);auto.
Qed.

Lemma crec:forall x n,  x^n <= (S x)^ n.
Proof.
induction n;auto.
simpl.
apply precrec.
auto.
Qed.

Lemma mayor_que_1:forall x n, 1<=x ->
                                             1<=  x^n.
Proof.
intros.
induction H.
rewrite uno;auto.
apply le_trans with ( m^n);try auto.
apply crec;auto.
Qed.

Lemma ev:forall x n,  x^(S n)=(x^n)*x.
Proof.
intros.
simpl.
auto.
Qed.

(*
Check nat_power 3.

Eval compute in (nat_power (2) 3).
*)

Fixpoint summation (f:nat->nat) (n:nat) {struct n} :nat :=
match n with
0 => f 0
| S p => f (S p)+(summation f p)
end.

Lemma aux:forall x n, summation (nat_power x )(S n)
           = nat_power x (S n)+summation (nat_power x) n.
Proof.
induction n; simpl;auto.
Qed.

(*
Definition g1 x n := (summation  (nat_power x ) (S n)).
Definition g2 x n := (summation (nat_power x) n)*x +1.
Eval compute in g1 2 3.
Eval compute in g2 2 3.
*)

Lemma distr: forall x n,(summation  (nat_power x ) ( S n))
                            =(summation (nat_power x) n)*x+1.
Proof.
intros.
induction n.
simpl.
trivial.


rewrite (aux x (S n)).
rewrite (aux x n).

rewrite (mult_plus_distr_r ).
rewrite ev.
rewrite aux in IHn.
rewrite IHn.
ring.
Qed.

(*
Definition G1 x n := (x-1)*(summation  (nat_power x ) n).
Definition G2 x n :=  (nat_power x (n+1)) -1.
Eval compute in G1 2 3.
Eval compute in G2 2 3.
*)

Lemma auxmasmenos:forall x y z, y<=x ->x-y=z -> x = y+z.
Proof.
intros.
rewrite <- H0.
apply le_plus_minus.
assumption.
Qed.

Lemma auxmenosmas:forall x y z, x=y+z -> x-y=z.
Proof.
intros.
rewrite H.
auto with arith.
Qed.

Lemma Sequal: forall n m, 1+n=1+m -> n=m.
Proof.
intros n m.
auto with arith.
Qed.

Lemma plus_reg_r:forall n m p, n+p=m+p -> n=m.
Proof.
intros n m p.
rewrite plus_comm.
rewrite (plus_comm m p).
apply plus_reg_l.
Qed.

Lemma equalS:forall n m, n+1=m+1->n=m.
Proof.
intros n m.
apply plus_reg_r.
Qed.

Lemma Splus:forall n, S n = n+1.
Proof.
intro n.
rewrite <- (plus_Snm_nSm n 0).
auto.
Qed.


Theorem sum_of_powers:forall (x:nat) (n:nat), 1 <= x  ->
 (x-1)*(summation  (nat_power x ) n) = ( x^(n+1)) -1.
Proof.
intros.
rewrite  mult_minus_distr_r.

replace (1*summation(nat_power x) n) with (summation(nat_power x) n);auto with arith.
apply auxmenosmas.

apply equalS.
rewrite <- plus_assoc.
replace (nat_power x (n + 1) - 1 + 1) with (nat_power x (n + 1)).
replace (n+1) with (S n).
rewrite mult_comm.
rewrite plus_comm.
2:ring.
symmetry.
rewrite plus_comm.
rewrite <- aux.
rewrite plus_comm.
apply  distr.
symmetry.
rewrite plus_comm.
symmetry.
apply le_plus_minus.
apply mayor_que_1.
auto.
Qed.




