Require Import ZArith Aux Even.

(* The record of operations *)

Structure fparams: Type := {
 K:> Set;               (* the scalar type *)
 v0: K;                (* 0 *)
 v1: K;                (* 1 *)
 eqK: K -> K -> bool;  (* = as a boolean function *)
 oppK: K -> K;         (* - unary *)
 addK : K -> K -> K;   (* + *)
 multK : K -> K -> K;  (* * *)
 invK : K -> K         (* 1/x *)
}.

(* Recover the usual mathematical notations *)

Delimit Scope field_scope with f.

Notation "x ?= y" := (eqK _ x y) (at level 70) : field_scope.
Notation "x + y" := (addK _ x y) : field_scope.
Notation "- x" := (oppK _ x) : field_scope.
Notation "x ^-1" := (invK _ x) (at level 25) : field_scope.
Notation "x * y" := (multK _ x y) : field_scope.
Notation "0" := (v0 _) : field_scope.
Notation "1" := (v1 _) : field_scope.

Section ParamsProp.

Variable p: fparams.
Open Scope field_scope.

(* Properties associated with a params *)
Structure fparamsProp: Type := {
 eqK_dec: forall x y: p, if x ?= y then x = y else x <> y;        
          (* Boolean equality *)
 addK_assoc: forall x y z: p, (x + y) + z = x + (y + z);
          (* Associativity for + *)
 addK_com: forall x y: p, x + y = y + x;
          (* Commutativity for + *)
 addK0l: forall x: p, 0 + x = x;
          (* Left neutral  for + *)
 oppKr: forall x: p, x + - x = 0;
          (* Right opposite  for + *)
 multK_assoc: forall x y z: p, (x * y) * z = x * (y * z);
          (* Associativity for * *)
 multK_com: forall x y: p, x * y = y * x;
          (* Commutativity for * *)
 multK1l: forall x: p, 1 * x = x;
          (* Left neutral element for * *)
 add_multKl: forall x y z: p, (x + y) * z = x * z + y * z;
          (* Left distributivity of + over * *)
 one_diff_zero: 1 <> 0 :> p;
          (* Inverse *)
 invKl: forall x: p, x <> 0 -> x * x^-1 = 1
}.

Fixpoint expK  (k: p) (n:nat) {struct n}: p := 
  match n with O => 1 | (S n1) => k * expK k n1 end.

Notation "x ^ k" := (expK x k) : field_scope.

(* Derived properties  *)

Variable Hp: fparamsProp.

Implicit Types x y z: p.

Lemma eqKI: forall x, x ?= x = true.
Proof.
(* Goal: forall x : K p, @eq bool (eqK p x x) true *)
intros x; generalize (eqK_dec Hp x x); case eqK; auto.
Qed.

Lemma eqK_spec x y: eq_Spec x y (x ?= y).
Proof.
(* Goal: @eq_Spec (K p) x y (eqK p x y) *)
generalize (eqK_dec Hp x y); case eqK; constructor; auto.
Qed.

(* Left oppositive for + *)
Lemma oppKl:  forall x, - x + x = 0.
Proof.
(* Goal: forall x : K p, @eq (K p) (addK p (oppK p x) x) (v0 p) *)
intros x; rewrite (addK_com Hp); rewrite (oppKr Hp); auto.
Qed.

(* Cancelation rule for + *)
Lemma addK_cancel x y z: x + y = x + z -> y = z.
Proof.
(* Goal: forall _ : @eq (K p) (multK p x y) (v0 p), or (@eq (K p) x (v0 p)) (@eq (K p) y (v0 p)) *)
intros H.
rewrite <- (addK0l Hp y);rewrite <- (oppKl x);rewrite (addK_assoc Hp); 
  rewrite H; rewrite <- (addK_assoc Hp); rewrite oppKl; 
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
  rewrite (addK0l Hp); auto.
Qed.

Lemma addK_eq_opp: forall x y, x + (-y) = 0 -> x = y.
Proof.
(* Goal: forall (x y : K p) (_ : @eq (K p) (addK p x (oppK p y)) (v0 p)), @eq (K p) x y *)
intros x y H; apply addK_cancel with (-y).
(* Goal: @eq (K p) (addK p (oppK p y) x) (addK p (oppK p y) y) *)
rewrite addK_com, H, addK_com, oppKr; auto.
Qed.

(* Right neutral for + *)
Lemma addK0r x: x + 0 = x.
Proof.
(* Goal: @eq (K p) (addK p x (v0 p)) x *)
intros; rewrite (addK_com Hp); rewrite (addK0l Hp); auto.
Qed.

(* Oppositive involutive *)
Lemma opp_oppK x: - (- x) = x.
Proof.
rewrite <- (addK0l Hp (- - x)); rewrite <- (oppKr Hp x); 
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
  rewrite (addK_assoc Hp); rewrite (oppKr Hp); rewrite addK0r; auto.
Qed.

(* Right neutral for * *)
Lemma multK1r x: x * 1 = x.
Proof.
(* Goal: @eq (K p) (multK p x (v1 p)) x *)
intros; rewrite (multK_com Hp); rewrite (multK1l Hp); auto.
Qed.

(* Right distributivity of + over * *)
Lemma add_multKr x y z: z * (x + y) = z * x + z * y.
Proof.
(* Goal: @eq (K p) (multK p z (addK p x y)) (addK p (multK p z x) (multK p z y)) *)
repeat rewrite (multK_com Hp z).
(* Goal: @eq (K p) (multK p (addK p x y) z) (addK p (multK p x z) (multK p y z)) *)
exact (add_multKl Hp x y z).
Qed.

(* 0 is its own opposite *)
Lemma oppK0: - 0 = 0 :> p.
Proof.
(* Goal: @eq (K p) (oppK p (v0 p)) (v0 p) *)
apply (addK_cancel 0); rewrite oppKr; try rewrite addK0l; auto.
Qed.

(* Distributivity of - over + *)
Lemma opp_addK x y: - (x + y) = - x + - y.
Proof.
(* Goal: @eq (K p) (oppK p (addK p x y)) (addK p (oppK p x) (oppK p y)) *)
apply (addK_cancel (x + y)).
rewrite (oppKr Hp); rewrite (addK_com Hp x); rewrite (addK_assoc Hp y); 
  rewrite <- (addK_assoc Hp x); rewrite (oppKr Hp); rewrite (addK0l Hp); 
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
  rewrite (oppKr Hp); auto.
Qed.

(* Right absorbent for * *)
Lemma multK0l x: 0 * x = 0.
Proof.
(* Goal: @eq (K p) (multK p (v0 p) x) (v0 p) *)
apply (addK_cancel (1 * x)).
(* Goal: @eq (K p) (addK p (multK p (v1 p) x) (multK p (v0 p) x)) (addK p (multK p (v1 p) x) (v0 p)) *)
rewrite <- (add_multKl Hp); rewrite addK0r; rewrite addK0r; auto.
Qed.

(* Left absorbent for * *)
Lemma multK0r x: x * 0 = 0.
Proof.
(* Goal: @eq (K p) (multK p x (v0 p)) (v0 p) *)
rewrite (multK_com Hp); rewrite multK0l; auto.
Qed.

(* Left distributivity of - over * *)
Lemma opp_multKl x y: - (x * y) = - x * y.
Proof.
(* Goal: @eq (K p) (oppK p (multK p x y)) (multK p x (oppK p y)) *)
apply (addK_cancel (x * y)).
rewrite (oppKr Hp); rewrite <- (add_multKl Hp); rewrite (oppKr Hp); 
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
  rewrite multK0l; auto.
Qed.

(* Right distributivity of - over * *)
Lemma opp_multKr x y: - (x * y) = x * - y.
Proof.
(* Goal: @eq (K p) (oppK p (multK p x y)) (multK p x (oppK p y)) *)
apply (addK_cancel (x * y)).
rewrite (oppKr Hp); rewrite <- add_multKr; rewrite (oppKr Hp);
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
  rewrite multK0r; auto.
Qed.

Lemma opp_multK1l x: - x  = (-(1)) * x.
Proof.
(* Goal: @eq (K p) (oppK p x) (multK p (oppK p (v1 p)) x) *)
rewrite <-opp_multKl, multK1l; auto.
Qed.

Lemma opp_multK1r x: - x  = x * (-(1)).
Proof.
(* Goal: @eq (K p) (oppK p x) (multK p x (oppK p (v1 p))) *)
rewrite <-opp_multKr, multK1r; auto.
Qed.

Lemma multK_m1_m1: -(1) * -(1) = 1 :>p.
Proof.
(* Goal: @eq (K p) (multK p (oppK p (v1 p)) (oppK p (v1 p))) (v1 p) *)
rewrite <-opp_multK1l, opp_oppK; auto.
Qed.

Lemma expKS n: (-(1)) ^n.+1 = -(-(1)) ^n.
Proof. intros; simpl; rewrite <-opp_multK1l; auto. Qed.

Lemma expK2m1 n: (-(1)) ^ n * (- (1)) ^  n =1.
Proof.
(* Goal: @eq (K p) (multK p (expK (oppK p (v1 p)) n) (expK (oppK p (v1 p)) n)) (v1 p) *)
induction n as [| n Hrec]; simpl; auto.
(* Goal: @eq (K p) (expK a n2) (multK p (v1 p) (expK a n2)) *)
(* Goal: @eq (K p) (multK p a (expK a (Init.Nat.add n1 n2))) (multK p (multK p a (expK a n1)) (expK a n2)) *)
rewrite multK1l; auto.
(* Goal: @eq (K p) (multK p (multK p (oppK p (v1 p)) (expK (oppK p (v1 p)) n)) (multK p (oppK p (v1 p)) (expK (oppK p (v1 p)) n))) (v1 p) *)
rewrite multK_assoc, (multK_com Hp (expK (- (1)) n)); auto.
(* Goal: @eq (K p) (multK p (oppK p (v1 p)) (multK p (multK p (oppK p (v1 p)) (expK (oppK p (v1 p)) n)) (expK (oppK p (v1 p)) n))) (v1 p) *)
repeat rewrite <- multK_assoc; auto.
(* Goal: @eq (K p) (multK p (multK p (multK p (oppK p (v1 p)) (oppK p (v1 p))) (expK (oppK p (v1 p)) n)) (expK (oppK p (v1 p)) n)) (v1 p) *)
rewrite multK_m1_m1, multK1l; auto.
Qed.

Lemma expK_add n1 n2 a: a ^ (n1 + n2) = a ^n1 * a ^ n2.
Proof.
(* Goal: @eq (K p) (expK a (Init.Nat.add n1 n2)) (multK p (expK a n1) (expK a n2)) *)
induction n1 as [| n1 Hrec]; simpl; auto.
(* Goal: @eq (K p) (expK a n2) (multK p (v1 p) (expK a n2)) *)
(* Goal: @eq (K p) (multK p a (expK a (Init.Nat.add n1 n2))) (multK p (multK p a (expK a n1)) (expK a n2)) *)
rewrite multK1l; auto.
(* Goal: @eq (K p) (multK p a (expK a (Init.Nat.add n1 n2))) (multK p (multK p a (expK a n1)) (expK a n2)) *)
rewrite Hrec, multK_assoc; auto.
Qed.

Lemma expKm1_even n: even n -> (-(1))^ n = 1
with expKm1_odd n: odd n -> (-(1))^ n = -(1).
Proof.
intros H; elim H; simpl; auto; clear n H.
intros n H; rewrite expKm1_odd; auto.
rewrite <-opp_multKr, multK1r, opp_oppK; auto.
intros H; elim H; simpl; auto; clear n H.
intros n H; rewrite expKm1_even; auto.
rewrite multK1r; auto.
Qed.

Lemma expKm1_sub m n: m <= n -> (-(1))^ (n - m) = (-(1))^ (n + m).
Proof.
(* Goal: forall _ : @eq (K p) (multK p x y) (v0 p), or (@eq (K p) x (v0 p)) (@eq (K p) y (v0 p)) *)
intros H.
(* Goal: @eq (K p) (expK (oppK p (v1 p)) (Init.Nat.sub n m)) (expK (oppK p (v1 p)) (Init.Nat.add n m)) *)
apply sym_equal; rewrite <-multK1l; auto.
(* Goal: @eq (K p) (expK (oppK p (v1 p)) (Init.Nat.add n m)) (multK p (v1 p) (expK (oppK p (v1 p)) (Init.Nat.sub n m))) *)
pattern (v1 p) at 2; rewrite <-expK2m1 with (n:= m).
rewrite <-!expK_add, <-Plus.plus_assoc, <-Minus.le_plus_minus, Plus.plus_comm;
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
  auto.
Qed.

Lemma expKm1_2 n: (-(1))^ (2 * n) = 1.
Proof. apply expKm1_even; auto with arith. Qed.

Lemma expKm1_2E n m: (-(1))^ (2 * n + m) = (-(1))^ m.
Proof. rewrite expK_add, expKm1_2, multK1l; auto. Qed.

Lemma invKr x: x <> 0 -> x^-1 * x = 1.
Proof.
(* Goal: forall _ : not (@eq (K p) x (v0 p)), @eq (K p) (multK p (invK p x) x) (v1 p) *)
intros Hx; rewrite multK_com; auto.
(* Goal: @eq (K p) (multK p x (invK p x)) (v1 p) *)
apply invKl; auto.
Qed.

(* Cancelation rule for * *)
Lemma multK_cancel x y z: x <> 0 -> x * y = x * z -> y = z.
Proof.
(* Goal: forall (_ : not (@eq (K p) x (v0 p))) (_ : @eq (K p) (multK p x y) (multK p x z)), @eq (K p) y z *)
intros Hx H.
(* Goal: @eq (K p) y z *)
rewrite <- multK1l; auto; rewrite <- (invKr _ Hx).
(* Goal: @eq (K p) y (multK p (multK p (invK p x) x) z) *)
rewrite multK_assoc; auto; rewrite <- H.
(* Goal: @eq (K p) (expK a n2) (multK p (v1 p) (expK a n2)) *)
(* Goal: @eq (K p) (multK p a (expK a (Init.Nat.add n1 n2))) (multK p (multK p a (expK a n1)) (expK a n2)) *)
rewrite <- multK_assoc; try rewrite invKr; try rewrite multK1l; auto.
Qed.

Lemma multK_swap x y z: x * (y * z) = y * (x * z).
Proof.
(* Goal: @eq (K p) (multK p x (multK p y z)) (multK p y (multK p x z)) *)
intros; rewrite <-!multK_assoc, (multK_com Hp x); auto.
Qed.

(* a field is integral *)
Lemma multK_integral x y : x * y = 0 -> x = 0 \/ y = 0.
Proof.
(* Goal: forall _ : @eq (K p) (multK p x y) (v0 p), or (@eq (K p) x (v0 p)) (@eq (K p) y (v0 p)) *)
intros H.
(* Goal: or (@eq (K p) x (v0 p)) (@eq (K p) y (v0 p)) *)
generalize (eqK_dec Hp x 0); case eqK; intros Hx; auto; right.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
apply (multK_cancel _ y  0 Hx); rewrite H; rewrite multK0r; auto.
Qed.

Lemma expK_integral x n : x^n = 0 -> x = 0.
Proof.
(* Goal: forall _ : @eq (K p) (multK p x y) (v0 p), or (@eq (K p) x (v0 p)) (@eq (K p) y (v0 p)) *)
induction n as [|n Hrec]; simpl; intros H.
(* Goal: @eq (K p) x (v0 p) *)
(* Goal: @eq (K p) x (v0 p) *)
case one_diff_zero; auto.
(* Goal: @eq (K p) x (v0 p) *)
case (multK_integral _ _ H); auto.
Qed.

Lemma expKm1_n0 n : (-(1))^n <> 0.
Proof.
(* Goal: @eq (K p) x (v0 p) *)
(* Goal: @eq (K p) x (v0 p) *)
intros H; case one_diff_zero; auto.
(* Goal: @eq (K p) (v1 p) (v0 p) *)
apply (addK_cancel (-(1))).
(* Goal: @eq (K p) (addK p (oppK p (v1 p)) (v1 p)) (addK p (oppK p (v1 p)) (v0 p)) *)
rewrite oppKl, addK0r.
(* Goal: @eq (K p) (v0 p) (oppK p (v1 p)) *)
apply sym_equal;apply expK_integral with (n := n); auto.
Qed.

Fixpoint n_to_K n := 
  match n with O => 0: p | S n => (1 + n_to_K n) end.

Lemma n_to_K0: n_to_K 0 = 0.
Proof. auto. Qed.

Lemma n_to_K1: n_to_K 1 = 1.
Proof. simpl; rewrite addK0r; auto. Qed.

Lemma n_to_K_add m n : n_to_K (m + n) = n_to_K m + n_to_K n.
Proof.
(* Goal: @eq (K p) (n_to_K (Init.Nat.mul m n)) (multK p (n_to_K m) (n_to_K n)) *)
elim m; simpl.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
rewrite addK0l; auto.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
intros m1 Hrec; rewrite Hrec, <-addK_assoc; auto.
Qed.

Lemma n_to_K_minus m n : n <= m -> n_to_K (m - n) = n_to_K m + -n_to_K n.
Proof.
(* Goal: forall _ : le n m, @eq (K p) (n_to_K (Init.Nat.sub m n)) (addK p (n_to_K m) (oppK p (n_to_K n))) *)
generalize n; clear n; elim m; simpl; clear m.
(* Goal: forall _ : @eq (K p) (multK p x y) (v0 p), or (@eq (K p) x (v0 p)) (@eq (K p) y (v0 p)) *)
intros [|n]; simpl; intros H.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
  rewrite oppKr; auto.
(* Goal: @eq (K p) (v0 p) (addK p (v0 p) (oppK p (addK p (v1 p) (n_to_K n)))) *)
(* Goal: forall (n : nat) (_ : forall (n0 : nat) (_ : le n0 n), @eq (K p) (n_to_K (Init.Nat.sub n n0)) (addK p (n_to_K n) (oppK p (n_to_K n0)))) (n0 : nat) (_ : le n0 (S n)), @eq (K p) (n_to_K match n0 with | O => S n | S l => Init.Nat.sub n l end) (addK p (addK p (v1 p) (n_to_K n)) (oppK p (n_to_K n0))) *)
contradict H; auto with arith.
(* Goal: forall _ : @eq (K p) (multK p x y) (v0 p), or (@eq (K p) x (v0 p)) (@eq (K p) y (v0 p)) *)
intros m Hrec [|n]; simpl; intros H.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
rewrite oppK0, addK0r; auto.
(* Goal: @eq (K p) (n_to_K (Init.Nat.sub m n)) (addK p (addK p (v1 p) (n_to_K m)) (oppK p (addK p (v1 p) (n_to_K n)))) *)
rewrite Hrec; auto with arith.
(* Goal: @eq (K p) (addK p (n_to_K m) (oppK p (n_to_K n))) (addK p (addK p (v1 p) (n_to_K m)) (oppK p (addK p (v1 p) (n_to_K n)))) *)
rewrite opp_addK.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
rewrite <-!addK_assoc, (addK_com Hp 1); auto.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
rewrite (addK_assoc Hp (n_to_K m)), oppKr, addK0r; auto.
Qed.

Lemma n_to_K_mult m n : n_to_K (m * n) = n_to_K m * n_to_K n.
Proof.
(* Goal: @eq (K p) (n_to_K (Init.Nat.mul m n)) (multK p (n_to_K m) (n_to_K n)) *)
elim m; simpl.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
rewrite multK0l; auto.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
intros m1 Hrec; rewrite n_to_K_add, add_multKl, multK1l, Hrec; auto.
Qed.

Definition Z_to_K (z: Z) :=
  match z with
  | Z0 => 0
  | Zpos _ => n_to_K (Z.abs_nat z)
  | Zneg _ => - (n_to_K (Z.abs_nat z))
  end.

Lemma Z_to_K_opp (z: Z): Z_to_K (-z)%Z = - Z_to_K z.
Proof. 
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
case z; simpl; auto.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
rewrite oppK0; auto.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
intros p1; rewrite opp_oppK; auto.
Qed.

Lemma Z_to_K_pos (z: Z): (0 <= z)%Z -> Z_to_K z = n_to_K (Z.abs_nat z).
Proof.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
case z; simpl; auto.
(* Goal: forall (p0 : positive) (_ : Z.le Z0 (Zneg p0)), @eq (K p) (oppK p (n_to_K (Pos.to_nat p0))) (n_to_K (Pos.to_nat p0)) *)
intros p1 H; contradict H; auto with zarith.
Qed.

Lemma Z_to_K_add (z1 z2: Z): 
  Z_to_K (z1 + z2)%Z = Z_to_K z1 + Z_to_K z2.
Proof.
assert (HH: 
 forall z1 z2 : Z, (0 <= z1)%Z -> (0 <= z2)%Z ->
   Z_to_K (z1 + z2) = Z_to_K z1 + Z_to_K z2).
(* Goal: forall (z1 z2 : Z) (_ : Z.le Z0 z1) (_ : Z.le Z0 z2), @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
intros z3 z4 Hz3 Hz.
(* Goal: @eq (K p) (Z_to_K (Z.add z3 z4)) (addK p (Z_to_K z3) (Z_to_K z4)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
rewrite !Z_to_K_pos, Zabs_nat_Zplus, n_to_K_add; auto with zarith.
assert (HH1: 
 forall z1 z2 : Z, (0 <= z1 <= z2)%Z ->
   Z_to_K (z2 - z1) = Z_to_K z2 + - Z_to_K z1).
(* Goal: forall (z1 z2 : Z) (_ : and (Z.le Z0 z1) (Z.le z1 z2)), @eq (K p) (Z_to_K (Z.sub z2 z1)) (addK p (Z_to_K z2) (oppK p (Z_to_K z1))) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
intros z3 z4 Hz3z4.
(* Goal: @eq (K p) (Z_to_K (Z.sub z4 z3)) (addK p (Z_to_K z4) (oppK p (Z_to_K z3))) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
rewrite !Z_to_K_pos, Zabs_nat_Zminus, n_to_K_minus; auto with zarith.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
apply Zabs_nat_le; auto.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
case (Zle_or_lt 0 z1); case (Zle_or_lt 0 z2); intros H2 H1; auto.
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
case (Zle_or_lt 0 (z1 + z2)); intros H3.
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
replace (z1 + z2)%Z with (z1 - (-z2))%Z; try ring.
(* Goal: @eq (K p) (Z_to_K (Z.sub z2 (Z.opp z1))) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
rewrite HH1; auto with zarith.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
rewrite Z_to_K_opp, opp_oppK; auto.
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
replace (z1 + z2)%Z with (-(-z2 - z1))%Z; try ring.
(* Goal: @eq (K p) (Z_to_K (Z.opp (Z.sub (Z.opp z1) z2))) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
rewrite Z_to_K_opp, HH1; auto with zarith.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
rewrite !Z_to_K_opp, opp_addK, !opp_oppK, addK_com; auto.
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
case (Zle_or_lt 0 (z1 + z2)); intros H3.
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
replace (z1 + z2)%Z with (z2 - (-z1))%Z; try ring.
(* Goal: @eq (K p) (Z_to_K (Z.sub z2 (Z.opp z1))) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
rewrite HH1; auto with zarith.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
rewrite Z_to_K_opp, opp_oppK, addK_com; auto.
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
replace (z1 + z2)%Z with (-(-z1 - z2))%Z; try ring.
(* Goal: @eq (K p) (Z_to_K (Z.opp (Z.sub (Z.opp z1) z2))) (addK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
rewrite Z_to_K_opp, HH1; auto with zarith.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
rewrite !Z_to_K_opp, opp_addK, !opp_oppK, addK_com; auto.
(* Goal: @eq (K p) (Z_to_K (Z.add z1 z2)) (addK p (Z_to_K z1) (Z_to_K z2)) *)
replace (z1 + z2)%Z with (-((-z1) + (-z2)))%Z; try ring.
(* Goal: @eq (K p) (Z_to_K (Z.opp (Z.add (Z.opp z1) (Z.opp z2)))) (addK p (Z_to_K z1) (Z_to_K z2)) *)
rewrite Z_to_K_opp, HH; auto with zarith.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
rewrite !Z_to_K_opp, opp_addK, !opp_oppK; auto.
Qed.

Lemma Z_to_K_minus (z1 z2: Z): 
  Z_to_K (z1 - z2)%Z = Z_to_K z1 + - Z_to_K z2.
Proof.
(* Goal: @eq (K p) (Z_to_K (Z.sub z1 z2)) (addK p (Z_to_K z1) (oppK p (Z_to_K z2))) *)
replace (z1 - z2)%Z with (z1 + -z2)%Z.
(* Goal: @eq (K p) (Z_to_K (Z.add z1 (Z.opp z2))) (addK p (Z_to_K z1) (oppK p (Z_to_K z2))) *)
(* Goal: @eq Z (Z.add z1 (Z.opp z2)) (Z.sub z1 z2) *)
rewrite Z_to_K_add, Z_to_K_opp; auto with zarith.
(* Goal: @eq Z (Z.add z1 (Z.opp z2)) (Z.sub z1 z2) *)
ring.
Qed.

Lemma Z_to_K_mult (z1 z2: Z): 
  Z_to_K (z1 * z2)%Z = Z_to_K z1 * Z_to_K z2.
Proof.
assert (HH: 
 forall z1 z2 : Z, (0 <= z1)%Z -> (0 <= z2)%Z ->
   Z_to_K (z1 * z2) = Z_to_K z1 * Z_to_K z2).
(* Goal: forall (z1 z2 : Z) (_ : Z.le Z0 z1) (_ : Z.le Z0 z2), @eq (K p) (Z_to_K (Z.mul z1 z2)) (multK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.mul z1 z2)) (multK p (Z_to_K z1) (Z_to_K z2)) *)
intros z3 z4 Hz3 Hz4.
(* Goal: @eq (K p) (Z_to_K (Z.mul z3 z4)) (multK p (Z_to_K z3) (Z_to_K z4)) *)
(* Goal: @eq (K p) (Z_to_K (Z.mul z1 z2)) (multK p (Z_to_K z1) (Z_to_K z2)) *)
rewrite !Z_to_K_pos; auto with zarith.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
rewrite Zabs_nat_mult, n_to_K_mult; auto.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
case (Zle_or_lt 0 z1); case (Zle_or_lt 0 z2); intros H2 H1; auto.
(* Goal: @eq Z (Z.add z1 (Z.opp z2)) (Z.sub z1 z2) *)
replace (z1 * z2)%Z with (-(z1 * (-z2)))%Z; try ring.
(* Goal: @eq (K p) (Z_to_K (Z.opp (Z.mul (Z.opp z1) z2))) (multK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.mul z1 z2)) (multK p (Z_to_K z1) (Z_to_K z2)) *)
rewrite Z_to_K_opp, HH, Z_to_K_opp; auto with zarith.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
rewrite opp_multKr, opp_oppK; auto.
(* Goal: @eq Z (Z.add z1 (Z.opp z2)) (Z.sub z1 z2) *)
replace (z1 * z2)%Z with (-(-z1 * z2))%Z; try ring.
(* Goal: @eq (K p) (Z_to_K (Z.opp (Z.mul (Z.opp z1) z2))) (multK p (Z_to_K z1) (Z_to_K z2)) *)
(* Goal: @eq (K p) (Z_to_K (Z.mul z1 z2)) (multK p (Z_to_K z1) (Z_to_K z2)) *)
rewrite Z_to_K_opp, HH, Z_to_K_opp; auto with zarith.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
rewrite opp_multKl, opp_oppK; auto.
(* Goal: @eq Z (Z.add z1 (Z.opp z2)) (Z.sub z1 z2) *)
replace (z1 * z2)%Z with (-z1 * -z2)%Z; try ring.
(* Goal: @eq (K p) (Z_to_K (Z.mul (Z.opp z1) (Z.opp z2))) (multK p (Z_to_K z1) (Z_to_K z2)) *)
rewrite HH, !Z_to_K_opp; auto with zarith.
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
rewrite <-opp_multKl, <-opp_multKr, opp_oppK; auto.
Qed.

End ParamsProp.

Notation "x ^ k" := (expK _ x%f k) : field_scope.

Ltac Krm0 :=
 repeat ((rewrite multK0l || rewrite multK0r || rewrite oppK0 ||
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
         rewrite addK0l || rewrite addK0r)); auto.

Ltac Krm1 :=
  Krm0; 
  repeat (rewrite multK1l || rewrite multK1r || rewrite <- opp_multKr ||
(* Goal: @eq (K p) (n_to_K O) (v0 p) *)
          rewrite expK2m1  || rewrite <- opp_multKl || rewrite opp_oppK); auto.


