Require Import Aux List Setoid Field VectorSpace.

Section Kn.

(* This is our scalar space with its dimension *)
Variable p : params.
(* The operations for scalar have the exprected properties *)
Hypothesis Hp : fparamsProp p.

(* We recover the usual mathematical notation *)
Notation "'K'" := (K p).

Delimit Scope kn_scope with k.
Open Scope vector_scope.
Open Scope kn_scope.

(* A vector is a list of length n *)

Fixpoint kn (n: nat): Set := 
  match n with O => unit | S n1 => (K * kn n1)%type end.


(** We first build the functions of the vector space *)

(* Equality of two vectors as list *)
Fixpoint eq (n : nat) : kn n -> kn n -> bool :=
  match n return (kn n -> kn n -> bool) with
  | 0%nat => fun a b => true
  | S n1 =>
      fun l1 l2 =>
      let (v1, l3) := l1 in
      let (v2, l4) := l2 in 
      if (v1 ?= v2)%f then eq n1 l3 l4 else false
  end.

(* Generate the constant k for the dimension n *)
Fixpoint genk (n: nat) (k: K) {struct n}: (kn n) :=
   match n return kn n with 0%nat => tt |  
                            (S n1) => (k, genk n1 k) end.

Notation " [ k ] " := (genk _ k) (at level 10): kn_scope.

(* Adding two vectors as list *)
Fixpoint add (n : nat) : kn n -> kn n -> kn n :=
  match n return (kn n -> kn n -> kn n) with
  | 0%nat => fun a b => tt
  | S n1 =>
      fun l1 l2 =>
      let (v1, l3) := l1 in
      let (v2, l4) := l2 in ((v1 + v2)%f, add n1 l3 l4)
  end.

(* Multiplication by a scalar *)
Fixpoint scal (n : nat) (k: K) {struct n}: kn n -> kn n :=
  match n return (kn n -> kn n) with
  | 0%nat => fun a => tt
  | S n1 =>
      fun l1 =>
      let (v1,l2) := l1 in ((k * v1)%f , scal n1 k l2)
  end.

Canonical Structure vn_eparams (n: nat) :=
  Build_eparams (kn n) K (genk n 0%f) (eq n) (add n) (scal n).

Definition fn n : vparamsProp (vn_eparams n).
(* Goal: vparamsProp (vn_eparams n) *)
apply Build_vparamsProp; auto.
(* eq Dec *)
(* Goal: @Logic.eq (Field.K (K p)) (pscal n x y) (pscal n y x) *)
induction n as [| n IH]; simpl.
(* Goal: forall x y : unit, @Logic.eq unit x y *)
(* Goal: forall x y : prod (Field.K (K p)) (kn n), if let (v1, l3) := x in let (v2, l4) := y in if eqK (K p) v1 v2 then eq n l3 l4 else false then @Logic.eq (prod (Field.K (K p)) (kn n)) x y else not (@Logic.eq (prod (Field.K (K p)) (kn n)) x y) *)
(* Goal: forall x y z : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (addE (vn_eparams n) (addE (vn_eparams n) x y) z) (addE (vn_eparams n) x (addE (vn_eparams n) y z)) *)
(* Goal: forall x y : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (addE (vn_eparams n) x y) (addE (vn_eparams n) y x) *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (addE (vn_eparams n) (E0 (vn_eparams n)) x) x *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (v0 (stype (vn_eparams n))) x) (E0 (vn_eparams n)) *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (v1 (stype (vn_eparams n))) x) x *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (addK (stype (vn_eparams n)) k1 k2) x) (addE (vn_eparams n) (scalE (vn_eparams n) k1 x) (scalE (vn_eparams n) k2 x)) *)
(* Goal: forall (k : Field.K (stype (vn_eparams n))) (x y : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) k (addE (vn_eparams n) x y)) (addE (vn_eparams n) (scalE (vn_eparams n) k x) (scalE (vn_eparams n) k y)) *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (multK (stype (vn_eparams n)) k1 k2) x) (scalE (vn_eparams n) k1 (scalE (vn_eparams n) k2 x)) *)
  intros [] []; auto.
intros (v1,l1) (v2, l2); 
(* Goal: @Logic.eq (Field.K (K p)) k (v0 (K p)) *)
  generalize (eqK_dec _ Hp v1 v2); case eqK; intros HH; subst.
(* Goal: if eq n l1 l2 then @Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) v2 l1) (@pair (Field.K (K p)) (kn n) v2 l2) else not (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) v2 l1) (@pair (Field.K (K p)) (kn n) v2 l2)) *)
(* Goal: not (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) v1 l1) (@pair (Field.K (K p)) (kn n) v2 l2)) *)
(* Goal: forall x y z : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (addE (vn_eparams n) (addE (vn_eparams n) x y) z) (addE (vn_eparams n) x (addE (vn_eparams n) y z)) *)
(* Goal: forall x y : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (addE (vn_eparams n) x y) (addE (vn_eparams n) y x) *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (addE (vn_eparams n) (E0 (vn_eparams n)) x) x *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (v0 (stype (vn_eparams n))) x) (E0 (vn_eparams n)) *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (v1 (stype (vn_eparams n))) x) x *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (addK (stype (vn_eparams n)) k1 k2) x) (addE (vn_eparams n) (scalE (vn_eparams n) k1 x) (scalE (vn_eparams n) k2 x)) *)
(* Goal: forall (k : Field.K (stype (vn_eparams n))) (x y : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) k (addE (vn_eparams n) x y)) (addE (vn_eparams n) (scalE (vn_eparams n) k x) (scalE (vn_eparams n) k y)) *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (multK (stype (vn_eparams n)) k1 k2) x) (scalE (vn_eparams n) k1 (scalE (vn_eparams n) k2 x)) *)
  generalize (IH l1 l2); unfold eqE; simpl.
(* Goal: forall _ : if eq n l1 l2 then @Logic.eq (kn n) l1 l2 else not (@Logic.eq (kn n) l1 l2), if eq n l1 l2 then @Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) v2 l1) (@pair (Field.K (K p)) (kn n) v2 l2) else not (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) v2 l1) (@pair (Field.K (K p)) (kn n) v2 l2)) *)
(* Goal: not (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) v1 l1) (@pair (Field.K (K p)) (kn n) v2 l2)) *)
(* Goal: forall x y z : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (addE (vn_eparams n) (addE (vn_eparams n) x y) z) (addE (vn_eparams n) x (addE (vn_eparams n) y z)) *)
(* Goal: forall x y : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (addE (vn_eparams n) x y) (addE (vn_eparams n) y x) *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (addE (vn_eparams n) (E0 (vn_eparams n)) x) x *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (v0 (stype (vn_eparams n))) x) (E0 (vn_eparams n)) *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (v1 (stype (vn_eparams n))) x) x *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (addK (stype (vn_eparams n)) k1 k2) x) (addE (vn_eparams n) (scalE (vn_eparams n) k1 x) (scalE (vn_eparams n) k2 x)) *)
(* Goal: forall (k : Field.K (stype (vn_eparams n))) (x y : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) k (addE (vn_eparams n) x y)) (addE (vn_eparams n) (scalE (vn_eparams n) k x) (scalE (vn_eparams n) k y)) *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (multK (stype (vn_eparams n)) k1 k2) x) (scalE (vn_eparams n) k1 (scalE (vn_eparams n) k2 x)) *)
case eq; intros HH; subst; auto.
(* Goal: not (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) v1 l1) (@pair (Field.K (K p)) (kn n) v2 l2)) *)
(* Goal: forall x y z : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (addE (vn_eparams n) (addE (vn_eparams n) x y) z) (addE (vn_eparams n) x (addE (vn_eparams n) y z)) *)
(* Goal: forall x y : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (addE (vn_eparams n) x y) (addE (vn_eparams n) y x) *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (addE (vn_eparams n) (E0 (vn_eparams n)) x) x *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (v0 (stype (vn_eparams n))) x) (E0 (vn_eparams n)) *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (v1 (stype (vn_eparams n))) x) x *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (addK (stype (vn_eparams n)) k1 k2) x) (addE (vn_eparams n) (scalE (vn_eparams n) k1 x) (scalE (vn_eparams n) k2 x)) *)
(* Goal: forall (k : Field.K (stype (vn_eparams n))) (x y : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) k (addE (vn_eparams n) x y)) (addE (vn_eparams n) (scalE (vn_eparams n) k x) (scalE (vn_eparams n) k y)) *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (multK (stype (vn_eparams n)) k1 k2) x) (scalE (vn_eparams n) k1 (scalE (vn_eparams n) k2 x)) *)
  intros HH1; injection HH1; intros; case HH; auto.
(* Goal: not (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) v1 l1) (@pair (Field.K (K p)) (kn n) v2 l2)) *)
(* Goal: forall x y z : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (addE (vn_eparams n) (addE (vn_eparams n) x y) z) (addE (vn_eparams n) x (addE (vn_eparams n) y z)) *)
(* Goal: forall x y : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (addE (vn_eparams n) x y) (addE (vn_eparams n) y x) *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (addE (vn_eparams n) (E0 (vn_eparams n)) x) x *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (v0 (stype (vn_eparams n))) x) (E0 (vn_eparams n)) *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (v1 (stype (vn_eparams n))) x) x *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (addK (stype (vn_eparams n)) k1 k2) x) (addE (vn_eparams n) (scalE (vn_eparams n) k1 x) (scalE (vn_eparams n) k2 x)) *)
(* Goal: forall (k : Field.K (stype (vn_eparams n))) (x y : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) k (addE (vn_eparams n) x y)) (addE (vn_eparams n) (scalE (vn_eparams n) k x) (scalE (vn_eparams n) k y)) *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (multK (stype (vn_eparams n)) k1 k2) x) (scalE (vn_eparams n) k1 (scalE (vn_eparams n) k2 x)) *)
intros HH1; injection HH1; intros; case HH; auto.
(* assoc *)
(* Goal: @Logic.eq (kn n) (kprod n (kprod n a b) c) (kprod n a (kprod n b c)) *)
induction n as [| n IH]; simpl; auto.
intros (v1,l3) (v2, l4) (v3, l5); simpl in IH; 
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
 rewrite IH, (addK_assoc _ Hp); auto.
(* comm *)
(* Goal: @Logic.eq (kn n) (kprod n (kprod n a b) c) (kprod n a (kprod n b c)) *)
induction n as [| n IH]; simpl; auto.
intros (v1,l3) (v2, l4); simpl in IH; 
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
  rewrite (addK_com _ Hp), (IH l3); auto.
(* 0 is  a left neutral element for + *)
(* Goal: @Logic.eq (kn n) (kprod n (kprod n a b) c) (kprod n a (kprod n b c)) *)
induction n as [| n IH]; simpl; auto.
(* Goal: forall x : unit, @Logic.eq unit tt x *)
(* Goal: forall x : prod (Field.K (K p)) (kn n), @Logic.eq (prod (Field.K (K p)) (kn n)) (let (v2, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) (v1 (K p)) v2) (scal n (v1 (K p)) l2)) x *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (addK (stype (vn_eparams n)) k1 k2) x) (addE (vn_eparams n) (scalE (vn_eparams n) k1 x) (scalE (vn_eparams n) k2 x)) *)
(* Goal: forall (k : Field.K (stype (vn_eparams n))) (x y : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) k (addE (vn_eparams n) x y)) (addE (vn_eparams n) (scalE (vn_eparams n) k x) (scalE (vn_eparams n) k y)) *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (multK (stype (vn_eparams n)) k1 k2) x) (scalE (vn_eparams n) k1 (scalE (vn_eparams n) k2 x)) *)
  intros []; auto.
(* Goal: forall x : prod (Field.K (K p)) (kn n), @Logic.eq (prod (Field.K (K p)) (kn n)) (let (v2, l4) := x in @pair (Field.K (K p)) (kn n) (addK (K p) (v0 (K p)) v2) (add n (genk n (v0 (K p))) l4)) x *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (v0 (stype (vn_eparams n))) x) (E0 (vn_eparams n)) *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (v1 (stype (vn_eparams n))) x) x *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (addK (stype (vn_eparams n)) k1 k2) x) (addE (vn_eparams n) (scalE (vn_eparams n) k1 x) (scalE (vn_eparams n) k2 x)) *)
(* Goal: forall (k : Field.K (stype (vn_eparams n))) (x y : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) k (addE (vn_eparams n) x y)) (addE (vn_eparams n) (scalE (vn_eparams n) k x) (scalE (vn_eparams n) k y)) *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (multK (stype (vn_eparams n)) k1 k2) x) (scalE (vn_eparams n) k1 (scalE (vn_eparams n) k2 x)) *)
intros (l1,l2); simpl in IH; rewrite (addK0l _ Hp), IH; auto.
(* Multiplication by 0 *)
(* Goal: @Logic.eq (kn n) (kprod n (kprod n a b) c) (kprod n a (kprod n b c)) *)
induction n as [| n IH]; simpl; auto.
(* Goal: forall x : prod (Field.K (K p)) (kn n), @Logic.eq (prod (Field.K (K p)) (kn n)) (let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) (v0 (K p)) v1) (scal n (v0 (K p)) l2)) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p)))) *)
(* Goal: forall x : E (vn_eparams n), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (v1 (stype (vn_eparams n))) x) x *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (addK (stype (vn_eparams n)) k1 k2) x) (addE (vn_eparams n) (scalE (vn_eparams n) k1 x) (scalE (vn_eparams n) k2 x)) *)
(* Goal: forall (k : Field.K (stype (vn_eparams n))) (x y : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) k (addE (vn_eparams n) x y)) (addE (vn_eparams n) (scalE (vn_eparams n) k x) (scalE (vn_eparams n) k y)) *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (multK (stype (vn_eparams n)) k1 k2) x) (scalE (vn_eparams n) k1 (scalE (vn_eparams n) k2 x)) *)
intros (l1, l2); simpl in IH; rewrite (multK0l _ Hp), IH; auto.
(* Multiplication by 1 *)
(* Goal: @Logic.eq (Field.K (K p)) (pscal n x y) (pscal n y x) *)
induction n as [| n IH]; simpl.
(* Goal: forall x : unit, @Logic.eq unit tt x *)
(* Goal: forall x : prod (Field.K (K p)) (kn n), @Logic.eq (prod (Field.K (K p)) (kn n)) (let (v2, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) (v1 (K p)) v2) (scal n (v1 (K p)) l2)) x *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (addK (stype (vn_eparams n)) k1 k2) x) (addE (vn_eparams n) (scalE (vn_eparams n) k1 x) (scalE (vn_eparams n) k2 x)) *)
(* Goal: forall (k : Field.K (stype (vn_eparams n))) (x y : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) k (addE (vn_eparams n) x y)) (addE (vn_eparams n) (scalE (vn_eparams n) k x) (scalE (vn_eparams n) k y)) *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (multK (stype (vn_eparams n)) k1 k2) x) (scalE (vn_eparams n) k1 (scalE (vn_eparams n) k2 x)) *)
  intros []; auto.
(* Goal: forall x : prod (Field.K (K p)) (kn n), @Logic.eq (prod (Field.K (K p)) (kn n)) (let (v2, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) (v1 (K p)) v2) (scal n (v1 (K p)) l2)) x *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (addK (stype (vn_eparams n)) k1 k2) x) (addE (vn_eparams n) (scalE (vn_eparams n) k1 x) (scalE (vn_eparams n) k2 x)) *)
(* Goal: forall (k : Field.K (stype (vn_eparams n))) (x y : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) k (addE (vn_eparams n) x y)) (addE (vn_eparams n) (scalE (vn_eparams n) k x) (scalE (vn_eparams n) k y)) *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (multK (stype (vn_eparams n)) k1 k2) x) (scalE (vn_eparams n) k1 (scalE (vn_eparams n) k2 x)) *)
intros (l1, l2); simpl in IH; rewrite (multK1l _ Hp), IH; auto.
(* Left addition of the multiplication by a scalar *)
(* Goal: @Logic.eq (kn n) (kprod n (kprod n a b) c) (kprod n a (kprod n b c)) *)
induction n as [| n IH]; simpl; auto.
(* Goal: forall (k1 k2 : Field.K (K p)) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (prod (Field.K (K p)) (kn n)) (let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) (addK (K p) k1 k2) v1) (scal n (addK (K p) k1 k2) l2)) (let (v1, l3) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k1 v1) (scal n k1 l2) in let (v2, l4) := let (v2, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k2 v2) (scal n k2 l2) in @pair (Field.K (K p)) (kn n) (addK (K p) v1 v2) (add n l3 l4)) *)
(* Goal: forall (k : Field.K (stype (vn_eparams n))) (x y : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) k (addE (vn_eparams n) x y)) (addE (vn_eparams n) (scalE (vn_eparams n) k x) (scalE (vn_eparams n) k y)) *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (multK (stype (vn_eparams n)) k1 k2) x) (scalE (vn_eparams n) k1 (scalE (vn_eparams n) k2 x)) *)
intros k1 k2 (l1, l2); simpl in IH; rewrite (add_multKl _ Hp), IH; auto.
(* Right addition of the multiplication by a scalar *)
(* Goal: @Logic.eq (kn n) (kprod n (kprod n a b) c) (kprod n a (kprod n b c)) *)
induction n as [| n IH]; simpl; auto.
(* Goal: forall (k : Field.K (K p)) (x y : prod (Field.K (K p)) (kn n)), @Logic.eq (prod (Field.K (K p)) (kn n)) (let (v1, l2) := let (v1, l3) := x in let (v2, l4) := y in @pair (Field.K (K p)) (kn n) (addK (K p) v1 v2) (add n l3 l4) in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2)) (let (v1, l3) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in let (v2, l4) := let (v2, l2) := y in @pair (Field.K (K p)) (kn n) (multK (K p) k v2) (scal n k l2) in @pair (Field.K (K p)) (kn n) (addK (K p) v1 v2) (add n l3 l4)) *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (multK (stype (vn_eparams n)) k1 k2) x) (scalE (vn_eparams n) k1 (scalE (vn_eparams n) k2 x)) *)
intros k (l1, l3) (l2, l4); simpl in IH; rewrite (add_multKr _ Hp), IH; auto.
(* Composition of the multiplication by a scalar *)
(* Goal: @Logic.eq (kn n) (kprod n (kprod n a b) c) (kprod n a (kprod n b c)) *)
induction n as [| n IH]; simpl; auto.
(* Goal: forall (k1 k2 : Field.K (K p)) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (prod (Field.K (K p)) (kn n)) (let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) (multK (K p) k1 k2) v1) (scal n (multK (K p) k1 k2) l2)) (let (v1, l2) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k2 v1) (scal n k2 l2) in @pair (Field.K (K p)) (kn n) (multK (K p) k1 v1) (scal n k1 l2)) *)
intros k1 k2 (k, x); simpl in IH; rewrite (multK_assoc _ Hp), IH; auto.
Qed.

Hint Resolve fn.

Ltac Kfold n :=
     change (add n) with (addE (vn_eparams n));
     change (scal n) with (scalE (vn_eparams n));
     change (genk n 0%f) with (E0 (vn_eparams n)).


(* scal is integral *)
Lemma scal_integral n k (x: kn n) : k .* x = 0 -> k = 0%f \/ x = 0.
Proof.
(* Goal: @Logic.eq (kn n) (kprod n (kprod n a b) c) (kprod n a (kprod n b c)) *)
induction n as [| n IH]; simpl; auto.
(* Goal: or (@Logic.eq unit x tt) (not (@Logic.eq unit x tt)) *)
(* Goal: or (@Logic.eq (prod (Field.K (K p)) (kn n)) x (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p))))) (not (@Logic.eq (prod (Field.K (K p)) (kn n)) x (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p)))))) *)
  destruct x; auto.
(* Goal: forall _ : @Logic.eq (prod (Field.K (K p)) (kn n)) (let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2)) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p)))), or (@Logic.eq (Field.K (K p)) k (v0 (K p))) (@Logic.eq (prod (Field.K (K p)) (kn n)) x (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p))))) *)
destruct x as (x1, x2); intros HH; injection HH; intros HH1 HH2.
(* Goal: or (@Logic.eq (Field.K (K p)) k (v0 (K p))) (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) x1 x2) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p))))) *)
case (IH _ _ HH1); case (multK_integral _ Hp k x1); auto.
(* Goal: forall (_ : @Logic.eq (Field.K (K p)) x1 (v0 (K p))) (_ : @Logic.eq (kn n) x2 (E0 (vn_eparams n))), or (@Logic.eq (Field.K (K p)) k (v0 (K p))) (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) x1 x2) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p))))) *)
intros; right; apply f_equal2 with (f := @pair _ _); auto.
Qed.

Lemma genk_inj n k1 k2 : [k1] = [k2] :> kn n.+1 -> k1 = k2.
Proof.
(* Goal: forall _ : @Logic.eq (kn (S n)) (genk (S n) k1) (genk (S n) k2), @Logic.eq (Field.K (K p)) k1 k2 *)
simpl; intros HH; injection HH; auto.
Qed.

Lemma genk0_dec n (x: kn n) :  x = 0 \/ x <> 0.
Proof.
(* Goal: @Logic.eq (kn n) (kprod n (kprod n a b) c) (kprod n a (kprod n b c)) *)
induction n as [| n IH]; simpl; auto.
(* Goal: or (@Logic.eq unit x tt) (not (@Logic.eq unit x tt)) *)
(* Goal: or (@Logic.eq (prod (Field.K (K p)) (kn n)) x (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p))))) (not (@Logic.eq (prod (Field.K (K p)) (kn n)) x (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p)))))) *)
destruct x; auto.
(* Goal: or (@Logic.eq (prod (Field.K (K p)) (kn n)) x (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p))))) (not (@Logic.eq (prod (Field.K (K p)) (kn n)) x (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p)))))) *)
destruct x as (x1, x2).
(* Goal: or (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) x1 x2) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p))))) (not (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) x1 x2) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p)))))) *)
case (IH x2); intros H1; subst; auto.
(* Goal: or (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) x1 (E0 (vn_eparams n))) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p))))) (not (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) x1 (E0 (vn_eparams n))) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p)))))) *)
(* Goal: or (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) x1 x2) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p))))) (not (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) x1 x2) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p)))))) *)
generalize (eqK_dec _ Hp x1 0%f); case eqK;intros H1; subst; auto.
(* Goal: or (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) x1 x2) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p))))) (not (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) x1 x2) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p)))))) *)
right; intro HH; case H1; injection HH; auto.
(* Goal: or (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) x1 x2) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p))))) (not (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) x1 x2) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (genk n (v0 (K p)))))) *)
right; intro HH; case H1; injection HH; auto.
Qed.

(* Conversion from list to kn *)
Fixpoint l2kn (n:nat) (l:list K) {struct l} : kn n:=
  match n return kn n with 
  | 0 => tt 
  | S n1 => match l with 
            | nil => genk (S n1) 0%f
            | a::l1 =>  (a,l2kn n1 l1)
            end
  end.

Fixpoint kn2l (n : nat) : kn n -> list K :=
  match n return (kn n -> list K) with
  | 0 => fun x => nil
  | S n1 => fun v => let (a, v1) := v in a :: kn2l n1 v1
  end.

Lemma kn2ll2knE n x : l2kn n (kn2l n x) = x.
Proof.
(* Goal: @Logic.eq (kn n) (l2kn n (kn2l n x)) x *)
induction n as [| n IH]; destruct x; simpl; auto.
(* Goal: @Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) k (l2kn n (kn2l n k0))) (@pair (Field.K (K p)) (kn n) k k0) *)
rewrite IH; auto.
Qed.

Lemma genk_id0 n i : In i (kn2l n (genk n 0%f)) -> i = 0%f.
Proof.
induction n as [| n IH]; simpl;
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
  intros HH; case HH; auto.
Qed.

Inductive eql_t0 : list K -> list K -> Prop :=
  eql_t0N: eql_t0 nil nil
| eql_t0Nl: forall l, eql_t0 l nil -> eql_t0 (0%f :: l) nil
| eql_t0Nr: forall l, eql_t0 nil l -> eql_t0 nil (0%f :: l) 
| eql_t0R: forall a l1 l2, eql_t0 l1 l2 -> eql_t0 (a :: l1) (a :: l2).

Hint Constructors eql_t0.

Lemma eql_refl l : eql_t0 l l.
Proof. elim l; auto. Qed.

Lemma eql_sym l1 l2 : eql_t0 l1 l2 -> eql_t0 l2 l1.
(* Goal: forall _ : eql_t0 l1 l2, eql_t0 l2 l1 *)
Proof. intros HH; elim HH; auto.
Qed.

Lemma eql_trans l2 l1 l3 : eql_t0 l1 l2 -> eql_t0 l2 l3 -> eql_t0 l1 l3.
Proof.
(* Goal: forall (_ : eql_t0 l1 l2) (_ : eql_t0 l2 l3), eql_t0 l1 l3 *)
intros HH; generalize l3; elim HH; auto; clear l1 l2 l3 HH.
(* Goal: forall (l : list (Field.K (K p))) (_ : eql_t0 (@nil (Field.K (K p))) l) (_ : forall (l3 : list (Field.K (K p))) (_ : eql_t0 l l3), eql_t0 (@nil (Field.K (K p))) l3) (l3 : list (Field.K (K p))) (_ : eql_t0 (@cons (Field.K (K p)) (v0 (K p)) l) l3), eql_t0 (@nil (Field.K (K p))) l3 *)
(* Goal: forall (a : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall (l3 : list (Field.K (K p))) (_ : eql_t0 l2 l3), eql_t0 l1 l3) (l3 : list (Field.K (K p))) (_ : eql_t0 (@cons (Field.K (K p)) a l2) l3), eql_t0 (@cons (Field.K (K p)) a l1) l3 *)
intros l1 HH IH l3 HH1.
(* Goal: eql_t0 (@cons (Field.K (K p)) (v0 (K p)) l1) l3 *)
(* Goal: forall (l : list (Field.K (K p))) (_ : eql_t0 (@nil (Field.K (K p))) l) (_ : forall (l3 : list (Field.K (K p))) (_ : eql_t0 l l3), eql_t0 (@nil (Field.K (K p))) l3) (l3 : list (Field.K (K p))) (_ : eql_t0 (@cons (Field.K (K p)) (v0 (K p)) l) l3), eql_t0 (@nil (Field.K (K p))) l3 *)
(* Goal: forall (a : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall (l3 : list (Field.K (K p))) (_ : eql_t0 l2 l3), eql_t0 l1 l3) (l3 : list (Field.K (K p))) (_ : eql_t0 (@cons (Field.K (K p)) a l2) l3), eql_t0 (@cons (Field.K (K p)) a l1) l3 *)
  generalize (IH _ HH1); inversion_clear HH1; auto.
(* Goal: forall (l : list (Field.K (K p))) (_ : eql_t0 (@nil (Field.K (K p))) l) (_ : forall (l3 : list (Field.K (K p))) (_ : eql_t0 l l3), eql_t0 (@nil (Field.K (K p))) l3) (l3 : list (Field.K (K p))) (_ : eql_t0 (@cons (Field.K (K p)) (v0 (K p)) l) l3), eql_t0 (@nil (Field.K (K p))) l3 *)
(* Goal: forall (a : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall (l3 : list (Field.K (K p))) (_ : eql_t0 l2 l3), eql_t0 l1 l3) (l3 : list (Field.K (K p))) (_ : eql_t0 (@cons (Field.K (K p)) a l2) l3), eql_t0 (@cons (Field.K (K p)) a l1) l3 *)
intros l1 HH IH l3 HH1.
(* Goal: eql_t0 (@cons (Field.K (K p)) a l1) l3 *)
  inversion_clear HH1; auto.
(* Goal: forall (a : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall (l3 : list (Field.K (K p))) (_ : eql_t0 l2 l3), eql_t0 l1 l3) (l3 : list (Field.K (K p))) (_ : eql_t0 (@cons (Field.K (K p)) a l2) l3), eql_t0 (@cons (Field.K (K p)) a l1) l3 *)
intros a l1 l2 HH IH l3 HH1.
(* Goal: eql_t0 (@cons (Field.K (K p)) a l1) l3 *)
  inversion_clear HH1; auto.
Qed.

Lemma dmap2_eql a l1 l2 l3 :
  eql_t0 l2 l3 -> 
  eql_t0 (dmap2 (multK K) a l1 l2) (dmap2 (multK K) a l1 l3).
Proof.
(* Goal: forall _ : eql_t0 l2 l3, eql_t0 (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l2) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l3) *)
intros HH; generalize l1; elim HH; clear l1 l2 l3 HH; simpl; auto.
(* Goal: forall l1 : list (Field.K (K p)), eql_t0 match l1 with | nil => @nil (Field.K (K p)) | cons a1 l3 => @nil (Field.K (K p)) end match l1 with | nil => @nil (Field.K (K p)) | cons a1 l3 => @nil (Field.K (K p)) end *)
(* Goal: forall (l : list (Field.K (K p))) (_ : eql_t0 l (@nil (Field.K (K p)))) (_ : forall l1 : list (Field.K (K p)), eql_t0 (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l) match l1 with | nil => @nil (Field.K (K p)) | cons a1 l3 => @nil (Field.K (K p)) end) (l1 : list (Field.K (K p))), eql_t0 match l1 with | nil => @cons (Field.K (K p)) (multK (K p) a (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l) | cons a1 l3 => @cons (Field.K (K p)) (multK (K p) a1 (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l) end match l1 with | nil => @nil (Field.K (K p)) | cons a1 l3 => @nil (Field.K (K p)) end *)
(* Goal: forall (l : list (Field.K (K p))) (_ : eql_t0 (@nil (Field.K (K p))) l) (_ : forall l1 : list (Field.K (K p)), eql_t0 match l1 with | nil => @nil (Field.K (K p)) | cons a1 l3 => @nil (Field.K (K p)) end (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l)) (l1 : list (Field.K (K p))), eql_t0 match l1 with | nil => @nil (Field.K (K p)) | cons a1 l3 => @nil (Field.K (K p)) end match l1 with | nil => @cons (Field.K (K p)) (multK (K p) a (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l) | cons a1 l3 => @cons (Field.K (K p)) (multK (K p) a1 (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l) end *)
(* Goal: forall (a0 : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall l3 : list (Field.K (K p)), eql_t0 (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l1) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l2)) (l3 : list (Field.K (K p))), eql_t0 match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l1) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l1) end match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l2) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l2) end *)
intros [|b l1]; auto.
(* Goal: forall (l : list (Field.K (K p))) (_ : eql_t0 (@nil (Field.K (K p))) l) (_ : forall l1 : list (Field.K (K p)), eql_t0 match l1 with | nil => @nil (Field.K (K p)) | cons a1 l3 => @nil (Field.K (K p)) end (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l)) (l1 : list (Field.K (K p))), eql_t0 match l1 with | nil => @nil (Field.K (K p)) | cons a1 l3 => @nil (Field.K (K p)) end match l1 with | nil => @cons (Field.K (K p)) (multK (K p) a (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l) | cons a1 l3 => @cons (Field.K (K p)) (multK (K p) a1 (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l) end *)
(* Goal: forall (a0 : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall l3 : list (Field.K (K p)), eql_t0 (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l1) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l2)) (l3 : list (Field.K (K p))), eql_t0 match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l1) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l1) end match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l2) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l2) end *)
intros l2 HH IH [|b l1].
(* Goal: eql_t0 (@cons (Field.K (K p)) (multK (K p) b (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l2)) (@nil (Field.K (K p))) *)
(* Goal: forall (l : list (Field.K (K p))) (_ : eql_t0 (@nil (Field.K (K p))) l) (_ : forall l1 : list (Field.K (K p)), eql_t0 match l1 with | nil => @nil (Field.K (K p)) | cons a1 l3 => @nil (Field.K (K p)) end (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l)) (l1 : list (Field.K (K p))), eql_t0 match l1 with | nil => @nil (Field.K (K p)) | cons a1 l3 => @nil (Field.K (K p)) end match l1 with | nil => @cons (Field.K (K p)) (multK (K p) a (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l) | cons a1 l3 => @cons (Field.K (K p)) (multK (K p) a1 (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l) end *)
(* Goal: forall (a0 : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall l3 : list (Field.K (K p)), eql_t0 (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l1) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l2)) (l3 : list (Field.K (K p))), eql_t0 match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l1) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l1) end match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l2) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l2) end *)
  rewrite multK0r; auto; apply eql_t0Nl.
(* Goal: eql_t0 (@nil (Field.K (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l2) *)
(* Goal: eql_t0 (@nil (Field.K (K p))) (@cons (Field.K (K p)) (multK (K p) b (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l2)) *)
(* Goal: forall (a0 : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall l3 : list (Field.K (K p)), eql_t0 (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l1) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l2)) (l3 : list (Field.K (K p))), eql_t0 match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l1) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l1) end match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l2) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l2) end *)
  generalize (IH nil); auto.
(* Goal: eql_t0 (@cons (Field.K (K p)) (multK (K p) b (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l2)) (@nil (Field.K (K p))) *)
(* Goal: forall (l : list (Field.K (K p))) (_ : eql_t0 (@nil (Field.K (K p))) l) (_ : forall l1 : list (Field.K (K p)), eql_t0 match l1 with | nil => @nil (Field.K (K p)) | cons a1 l3 => @nil (Field.K (K p)) end (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l)) (l1 : list (Field.K (K p))), eql_t0 match l1 with | nil => @nil (Field.K (K p)) | cons a1 l3 => @nil (Field.K (K p)) end match l1 with | nil => @cons (Field.K (K p)) (multK (K p) a (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l) | cons a1 l3 => @cons (Field.K (K p)) (multK (K p) a1 (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l) end *)
(* Goal: forall (a0 : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall l3 : list (Field.K (K p)), eql_t0 (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l1) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l2)) (l3 : list (Field.K (K p))), eql_t0 match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l1) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l1) end match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l2) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l2) end *)
  rewrite multK0r; auto; apply eql_t0Nl.
(* Goal: eql_t0 (@nil (Field.K (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l2) *)
(* Goal: forall (a0 : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall l3 : list (Field.K (K p)), eql_t0 (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l1) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l2)) (l3 : list (Field.K (K p))), eql_t0 match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l1) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l1) end match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l2) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l2) end *)
  generalize (IH l1); auto; case l1; auto.
(* Goal: forall (l : list (Field.K (K p))) (_ : eql_t0 (@nil (Field.K (K p))) l) (_ : forall l1 : list (Field.K (K p)), eql_t0 match l1 with | nil => @nil (Field.K (K p)) | cons a1 l3 => @nil (Field.K (K p)) end (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l)) (l1 : list (Field.K (K p))), eql_t0 match l1 with | nil => @nil (Field.K (K p)) | cons a1 l3 => @nil (Field.K (K p)) end match l1 with | nil => @cons (Field.K (K p)) (multK (K p) a (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l) | cons a1 l3 => @cons (Field.K (K p)) (multK (K p) a1 (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l) end *)
(* Goal: forall (a0 : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall l3 : list (Field.K (K p)), eql_t0 (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l1) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l2)) (l3 : list (Field.K (K p))), eql_t0 match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l1) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l1) end match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l2) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l2) end *)
intros l2 HH IH [|b l1].
(* Goal: eql_t0 (@nil (Field.K (K p))) (@cons (Field.K (K p)) (multK (K p) b (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l2)) *)
(* Goal: forall (a0 : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall l3 : list (Field.K (K p)), eql_t0 (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l1) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l2)) (l3 : list (Field.K (K p))), eql_t0 match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l1) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l1) end match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l2) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l2) end *)
  rewrite multK0r; auto; apply eql_t0Nr.
(* Goal: eql_t0 (@nil (Field.K (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l2) *)
(* Goal: eql_t0 (@nil (Field.K (K p))) (@cons (Field.K (K p)) (multK (K p) b (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l2)) *)
(* Goal: forall (a0 : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall l3 : list (Field.K (K p)), eql_t0 (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l1) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l2)) (l3 : list (Field.K (K p))), eql_t0 match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l1) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l1) end match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l2) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l2) end *)
  generalize (IH nil); auto.
(* Goal: eql_t0 (@nil (Field.K (K p))) (@cons (Field.K (K p)) (multK (K p) b (v0 (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l2)) *)
(* Goal: forall (a0 : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall l3 : list (Field.K (K p)), eql_t0 (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l1) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l2)) (l3 : list (Field.K (K p))), eql_t0 match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l1) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l1) end match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l2) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l2) end *)
  rewrite multK0r; auto; apply eql_t0Nr.
(* Goal: eql_t0 (@nil (Field.K (K p))) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l2) *)
(* Goal: forall (a0 : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall l3 : list (Field.K (K p)), eql_t0 (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l1) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l2)) (l3 : list (Field.K (K p))), eql_t0 match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l1) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l1) end match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l2) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l2) end *)
  generalize (IH l1); auto; case l1; auto.
(* Goal: forall (a0 : Field.K (K p)) (l1 l2 : list (Field.K (K p))) (_ : eql_t0 l1 l2) (_ : forall l3 : list (Field.K (K p)), eql_t0 (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l1) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l3 l2)) (l3 : list (Field.K (K p))), eql_t0 match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l1) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l1) end match l3 with | nil => @cons (Field.K (K p)) (multK (K p) a a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a (@nil (Field.K (K p))) l2) | cons a1 l4 => @cons (Field.K (K p)) (multK (K p) a1 a0) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l4 l2) end *)
intros b l2 l3 HH IH [|c l1].
(* Goal: eql_t0 (@cons (Field.K (K p)) (multK (K p) c b) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l2)) (@cons (Field.K (K p)) (multK (K p) c b) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l3)) *)
 apply eql_t0R; auto.
(* Goal: eql_t0 (@cons (Field.K (K p)) (multK (K p) c b) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l2)) (@cons (Field.K (K p)) (multK (K p) c b) (@dmap2 (Field.K (K p)) (Field.K (K p)) (Field.K (K p)) (multK (K p)) a l1 l3)) *)
 apply eql_t0R; auto.
Qed.

Lemma kn2l_0 n : eql_t0 (kn2l n 0) nil.
Proof. elim n; simpl; auto. Qed.

(* Generate the p element of the base in dimension n *)
Fixpoint gen (n: nat) (p: nat) {struct n} : kn n :=
  match n return kn n with O => tt | S n1 =>
    match p with
      0 => (1%f, genk n1 0%f)
    | S p1 =>  (0%f, gen n1 p1) 
    end
  end.

Notation " 'e_ p" := (gen _ p) (at level 70): kn_scope.

Lemma gen_inj n p1 p2 : p1 < n -> p2 < n ->
  'e_p1 = ('e_p2 : kn n)  -> p1 = p2.
Proof.
(* Goal: forall (_ : lt p1 n) (_ : lt p2 n) (_ : @Logic.eq (kn n) (gen n p1) (gen n p2 : kn n)), @Logic.eq nat p1 p2 *)
generalize p1 p2; clear p1 p2.
(* Goal: forall (p1 p2 : nat) (_ : lt p1 n) (_ : lt p2 n) (_ : @Logic.eq (kn n) (gen n p1) (gen n p2)), @Logic.eq nat p1 p2 *)
induction n as [| n IH]; auto.
(* Goal: forall (p1 p2 : nat) (_ : lt p1 O) (_ : lt p2 O) (_ : @Logic.eq (kn O) (gen O p1) (gen O p2)), @Logic.eq nat p1 p2 *)
(* Goal: forall (p1 p2 : nat) (_ : lt p1 (S n)) (_ : lt p2 (S n)) (_ : @Logic.eq (kn (S n)) (gen (S n) p1) (gen (S n) p2)), @Logic.eq nat p1 p2 *)
intros p1 p2 Hp1; contradict Hp1; auto with arith.
(* Goal: forall (p1 p2 : nat) (_ : lt p1 (S n)) (_ : lt p2 (S n)) (_ : @Logic.eq (kn (S n)) (gen (S n) p1) (gen (S n) p2)), @Logic.eq nat p1 p2 *)
intros [|p1] [|p2] HH1 HH2; simpl; auto.
(* Goal: forall _ : @Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (gen n p1)) (@pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p)))), @Logic.eq nat (S p1) O *)
(* Goal: forall _ : @Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (gen n p1)) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (gen n p2)), @Logic.eq nat (S p1) (S p2) *)
intros HH; injection HH; intros; case (one_diff_zero _ Hp); auto.
(* Goal: forall _ : @Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (gen n p1)) (@pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p)))), @Logic.eq nat (S p1) O *)
(* Goal: forall _ : @Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (gen n p1)) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (gen n p2)), @Logic.eq nat (S p1) (S p2) *)
intros HH; injection HH; intros; case (one_diff_zero _ Hp); auto.
(* Goal: forall _ : @Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (gen n p1)) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (gen n p2)), @Logic.eq nat (S p1) (S p2) *)
intros HH; rewrite (IH p1 p2); auto with arith.
(* Goal: @Logic.eq (kn n) (gen n p1) (gen n p2) *)
injection HH; auto.
Qed.

Lemma kn2l_e0 n : eql_t0 (kn2l n.+1 ('e_0)) (1%f :: nil).
Proof. 
(* Goal: eql_t0 (kn2l (S n) (gen (S n) O)) (@cons (Field.K (K p)) (v1 (K p)) (@nil (Field.K (K p)))) *)
simpl; auto.
(* Goal: eql_t0 (@cons (Field.K (K p)) (v1 (K p)) (kn2l n (genk n (v0 (K p))))) (@cons (Field.K (K p)) (v1 (K p)) (@nil (Field.K (K p)))) *)
apply eql_t0R.
(* Goal: eql_t0 (kn2l n (genk n (v0 (K p)))) (@nil (Field.K (K p))) *)
apply kn2l_0; auto.
Qed.

Lemma kn2l_ei n i :
  eql_t0 (kn2l n.+1 ('e_i.+1))  (0%f :: kn2l n ('e_i)).
Proof.
(* Goal: eql_t0 (kn2l (S n) (gen (S n) (S i))) (@cons (Field.K (K p)) (v0 (K p)) (kn2l n (gen n i))) *)
apply eql_refl.
Qed.

(* Lift a vector of dimension n into a vector of dimension n+1 whose
   first component is 0 *)
Definition lift (n: nat) (v: kn n) : (kn (S n)) :=  (0%f, v).

Lemma lift0 n : lift n 0 = 0.
Proof. auto. Qed.

(* Lift of generator of the base *)
Lemma lift_e : forall n i, 'e_(S i) = lift n ('e_i).
Proof. auto. Qed.

(* Lift on add *)
Lemma lift_add n x y : lift n (x + y) = lift n x + lift n y.
Proof. unfold lift; simpl; rewrite addK0l; auto. Qed.

(* Lift on scalar multiplication *)
Lemma lift_scal n k x :  lift n (k .* x) = scalE (vn_eparams (S n)) k (lift n x).
Proof. unfold lift; simpl; rewrite multK0r; auto. Qed.

(* Lift on the multiple product *)
Lemma lift_mprod (n: nat) ks vs : ks *X* map (lift n) vs =
  lift n (mprod (vn_eparams n) ks vs).
Proof.
(* Goal: @Logic.eq (E (vn_eparams (S n))) (mprod (vn_eparams (S n)) ks (@map (kn n) (kn (S n)) (lift n) vs)) (lift n (mprod (vn_eparams n) ks vs)) *)
generalize vs; clear vs; induction ks as [| k ks IH].
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
  intros vs; repeat rewrite mprod0l; auto.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
intros [| v vs]; simpl; try rewrite mprod0r; auto.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
rewrite (mprod_S (vn_eparams n.+1)); auto.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
rewrite mprod_S; auto.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
rewrite IH, lift_add, lift_scal; auto.
Qed.

(* The base as the list of all the generators *)
Fixpoint base (n : nat) : list (kn n) :=
  match n return list (kn n) with
  | 0 => nil
  | S n1 => ('e_0: kn (S n1)) :: map (lift n1) (base n1)
  end.

(* Each generator is in the base *)
Lemma e_in_base n i : i < n -> In ('e_i) (base n).
Proof.
(* Goal: forall _ : lt i n, @In (kn n) (gen n i) (base n) *)
generalize i; clear i; induction n as [| n IH].
(* Goal: forall (i : nat) (_ : lt i O), @In (kn O) (gen O i) (base O) *)
(* Goal: forall (i : nat) (_ : lt i (S n)), @In (kn (S n)) (gen (S n) i) (base (S n)) *)
  intros i HH; contradict HH; auto with arith.
(* Goal: forall (i : nat) (_ : lt i (S n)), @In (kn (S n)) (gen (S n) i) (base (S n)) *)
intros [| p1] Hp1; simpl; Kfold n; auto; right.
(* Goal: @In (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) (v0 (K p)) (gen n p1)) (@map (kn n) (prod (Field.K (K p)) (kn n)) (lift n) (base n)) *)
refine (in_map _ _ _ _); auto with arith.
Qed.

(* An element of the base is a generator *)
Lemma e_in_base_ex n v : 
  In v (base n) -> exists p1, p1 < n /\ v = 'e_p1.
Proof.
(* Goal: @Logic.eq (E (vn_eparams n)) (mprod (vn_eparams n) (kn2l n v) (base n)) v *)
generalize v; clear v; induction n as [| n IH].
(* Goal: forall (v : kn O) (_ : @In (kn O) v (base O)), @ex nat (fun p1 : nat => and (lt p1 O) (@Logic.eq (kn O) v (gen O p1))) *)
(* Goal: forall (v : kn (S n)) (_ : @In (kn (S n)) v (base (S n))), @ex nat (fun p1 : nat => and (lt p1 (S n)) (@Logic.eq (kn (S n)) v (gen (S n) p1))) *)
  intros v [].
(* Goal: forall (v : kn (S n)) (_ : @In (kn (S n)) v (base (S n))), @ex nat (fun p1 : nat => and (lt p1 (S n)) (@Logic.eq (kn (S n)) v (gen (S n) p1))) *)
simpl; intros [vv1 vv2] [H1 | H1].
(* Goal: @ex nat (fun p1 : nat => and (lt p1 (S n)) (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) vv1 vv2) match p1 with | O => @pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p))) | S p2 => @pair (Field.K (K p)) (kn n) (v0 (K p)) (gen n p2) end)) *)
(* Goal: @ex nat (fun p1 : nat => and (lt p1 (S n)) (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) vv1 vv2) match p1 with | O => @pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p))) | S p2 => @pair (Field.K (K p)) (kn n) (v0 (K p)) (gen n p2) end)) *)
  exists 0%nat; auto with arith.
(* Goal: @ex nat (fun p1 : nat => and (lt p1 (S n)) (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) vv1 vv2) match p1 with | O => @pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p))) | S p2 => @pair (Field.K (K p)) (kn n) (v0 (K p)) (gen n p2) end)) *)
rewrite in_map_iff in H1; case H1.
(* Goal: forall (x : kn n) (_ : and (@Logic.eq (prod (Field.K (K p)) (kn n)) (lift n x) (@pair (Field.K (K p)) (kn n) vv1 vv2)) (@In (kn n) x (base n))), @ex nat (fun p1 : nat => and (lt p1 (S n)) (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) vv1 vv2) match p1 with | O => @pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p))) | S p2 => @pair (Field.K (K p)) (kn n) (v0 (K p)) (gen n p2) end)) *)
intros vv3 [Hvv3 Hvv3'].
(* Goal: @ex nat (fun p1 : nat => and (lt p1 (S n)) (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) vv1 vv2) match p1 with | O => @pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p))) | S p2 => @pair (Field.K (K p)) (kn n) (v0 (K p)) (gen n p2) end)) *)
case (IH _ Hvv3'); intros p1 [Hp1 Hp2].
(* Goal: @ex nat (fun p1 : nat => and (lt p1 (S n)) (@Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) vv1 vv2) match p1 with | O => @pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p))) | S p2 => @pair (Field.K (K p)) (kn n) (v0 (K p)) (gen n p2) end)) *)
exists (S p1); split; auto with arith.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
rewrite <- Hvv3; rewrite Hp2; auto.
Qed.

(* The length of the base is n *)
Lemma base_length n : length (base n) = n.
Proof.
(* Goal: @Logic.eq (kn n) (kprod n (kprod n a b) c) (kprod n a (kprod n b c)) *)
induction n as [| n IH]; simpl; auto.
(* Goal: @Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) k (l2kn n (kn2l n k0))) (@pair (Field.K (K p)) (kn n) k k0) *)
rewrite map_length; rewrite IH; auto.
Qed.

(* The base is free *)
Lemma base_free n : free _ (base n).
Proof.
(* Goal: forall (i j : nat) (_ : lt i n) (_ : lt j n), @Logic.eq (Field.K (K p)) (pscal n (gen n i) (gen n j)) (if eq_nat i j then v1 (K p) else v0 (K p)) *)
  induction n as [|n IH].
  *
(* Goal: free (vn_eparams (S n)) (base (S n)) *)
     intro. simpl. intros H H0 k H1.
(* Goal: @Logic.eq (Field.K (K p)) k (v0 (K p)) *)
    assert (ks = nil) by (destruct ks; auto; discriminate).  subst.  inversion H1. 
  * intro. destruct ks as [| k ks].
(* Goal: forall (_ : @Logic.eq (E (vn_eparams (S n))) (addE (vn_eparams (S n)) (scalE (vn_eparams (S n)) k (@pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p))))) (lift n (mprod (vn_eparams n) ks (base n)))) (E0 (vn_eparams (S n)))) (k0 : Field.K (stype (vn_eparams (S n)))) (_ : @In (Field.K (stype (vn_eparams (S n)))) k0 (@cons (Field.K (stype (vn_eparams (S n)))) k ks)), @Logic.eq (Field.K (stype (vn_eparams (S n)))) k0 (v0 (stype (vn_eparams (S n)))) *)
  - simpl. intros. discriminate.
  -
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
    intros H1. simpl base. rewrite mprod_S, lift_mprod; auto.
(* Goal: forall (_ : @Logic.eq (E (vn_eparams (S n))) (addE (vn_eparams (S n)) (scalE (vn_eparams (S n)) k (@pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p))))) (lift n (mprod (vn_eparams n) ks (base n)))) (E0 (vn_eparams (S n)))) (k0 : Field.K (stype (vn_eparams (S n)))) (_ : @In (Field.K (stype (vn_eparams (S n)))) k0 (@cons (Field.K (stype (vn_eparams (S n)))) k ks)), @Logic.eq (Field.K (stype (vn_eparams (S n)))) k0 (v0 (stype (vn_eparams (S n)))) *)
    simpl. intros HH. injection HH. clear HH.
(* Goal: forall (_ : @Logic.eq (kn n) (add n (scal n k (genk n (v0 (K p)))) (mprod (vn_eparams n) ks (base n))) (genk n (v0 (K p)))) (_ : @Logic.eq (Field.K (K p)) (addK (K p) (multK (K p) k (v1 (K p))) (v0 (K p))) (v0 (K p))) (k0 : Field.K (K p)) (_ : or (@Logic.eq (Field.K (K p)) k k0) (@In (Field.K (K p)) k0 ks)), @Logic.eq (Field.K (K p)) k0 (v0 (K p)) *)
    Kfold n.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
    rewrite scalE0r, addE0l, addK0r; auto.
(* Goal: forall (_ : @Logic.eq (kn n) (mprod (vn_eparams n) ks (base n)) (E0 (vn_eparams n))) (_ : @Logic.eq (Field.K (K p)) (multK (K p) k (v1 (K p))) (v0 (K p))) (k0 : Field.K (K p)) (_ : or (@Logic.eq (Field.K (K p)) k k0) (@In (Field.K (K p)) k0 ks)), @Logic.eq (Field.K (K p)) k0 (v0 (K p)) *)
    intros H2 H3 k1 [Hk1 | Hk1].
    +
(* Goal: @Logic.eq (Field.K (K p)) k1 (v0 (K p)) *)
      case (multK_integral _ Hp _ _ H3); try subst; auto; intros Heq.
(* Goal: @Logic.eq (Field.K (K p)) k1 (v0 (K p)) *)
      case (one_diff_zero (vn_eparams n)); auto; apply (vgenk_inj _ _ _ Heq).
    +
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
      injection H1; rewrite map_length; auto.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
      intros Hl; apply (IH ks); auto.
Qed.


Lemma k2l_mprod n (v: kn n) : kn2l n v *X* base n = v.
Proof.
(* Goal: @Logic.eq (E (vn_eparams n)) (mprod (vn_eparams n) (kn2l n v) (base n)) v *)
generalize v; clear v; induction n as [| n IH].
(* Goal: forall x : unit, @Logic.eq unit tt x *)
(* Goal: forall x : prod (Field.K (K p)) (kn n), @Logic.eq (prod (Field.K (K p)) (kn n)) (let (v2, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) (v1 (K p)) v2) (scal n (v1 (K p)) l2)) x *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (addK (stype (vn_eparams n)) k1 k2) x) (addE (vn_eparams n) (scalE (vn_eparams n) k1 x) (scalE (vn_eparams n) k2 x)) *)
(* Goal: forall (k : Field.K (stype (vn_eparams n))) (x y : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) k (addE (vn_eparams n) x y)) (addE (vn_eparams n) (scalE (vn_eparams n) k x) (scalE (vn_eparams n) k y)) *)
(* Goal: forall (k1 k2 : Field.K (stype (vn_eparams n))) (x : E (vn_eparams n)), @Logic.eq (E (vn_eparams n)) (scalE (vn_eparams n) (multK (stype (vn_eparams n)) k1 k2) x) (scalE (vn_eparams n) k1 (scalE (vn_eparams n) k2 x)) *)
simpl; intros []; auto.
(* Goal: forall v : kn (S n), @Logic.eq (E (vn_eparams (S n))) (mprod (vn_eparams (S n)) (kn2l (S n) v) (base (S n))) v *)
simpl; intros (x, v).
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
rewrite (mprod_S (vn_eparams n.+1)); auto.
(* Goal: @Logic.eq (prod (Field.K (K p)) (kn n)) (addE (vn_eparams (S n)) (scalE (vn_eparams (S n)) x (@pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p))))) (mprod (vn_eparams (S n)) (kn2l n v) (@map (kn n) (prod (Field.K (K p)) (kn n)) (lift n) (base n)))) (@pair (Field.K (K p)) (kn n) x v) *)
rewrite lift_mprod, IH.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
simpl; Kfold n; auto.
(* Goal: @Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) (addK (K p) (multK (K p) x (v1 (K p))) (v0 (K p))) (addE (vn_eparams n) (scalE (vn_eparams n) x (E0 (vn_eparams n))) v)) (@pair (Field.K (K p)) (kn n) x v) *)
Krm1; Vrm0.
Qed.

(* Every vector is a linear combination of the base *)
Lemma cbl_base n v : cbl _ (base n) v.
Proof. rewrite <- (k2l_mprod n v); apply mprod_cbl; auto. Qed.

Lemma  kn_induct n (P: kn n -> Prop) :
     P 0 -> 
     (forall p, p < n -> P ('e_p)) ->
     (forall v1 v2, P v1 -> P v2 -> P (v1 + v2)) ->
     (forall k v, P v -> P (k .* v)) ->
     (forall x, P x).
Proof.
(* Goal: forall (_ : P (E0 (vn_eparams n))) (_ : forall (p : nat) (_ : lt p n), P (gen n p)) (_ : forall (v1 v2 : kn n) (_ : P v1) (_ : P v2), P (addE (vn_eparams n) v1 v2)) (_ : forall (k : Field.K (stype (vn_eparams n))) (v : kn n) (_ : P v), P (scalE (vn_eparams n) k v)) (x : kn n), P x *)
intros H1 H2 H3 H4 x.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
elim (cbl_base n x); clear x; auto.
(* Goal: forall (v : E (vn_eparams n)) (_ : @In (E (vn_eparams n)) v (base n)), P v *)
intros v HH; case (e_in_base_ex _ _ HH); intros m (Hl,Hm).
(* Goal: P v *)
rewrite Hm; auto with arith.
Qed.

(* Coordinates for k vector *)
Fixpoint proj (n: nat) k : (kn n) -> K :=
  match n return kn n -> K with 
  | O => fun _ => 0%f
  | S n1 => fun l => let (a,l1) := l in 
          match k with | O => a | S k1 => 
           proj n1 k1 l1
          end
  end.

Lemma proj0 n i : proj n i 0 = 0%f.
Proof.
(* Goal: @Logic.eq (Field.K (K p)) (proj n i (E0 (vn_eparams n))) (v0 (K p)) *)
generalize i; clear i.
(* Goal: eql_t0 (kn2l (S n) (gen (S n) O)) (@cons (Field.K (K p)) (v1 (K p)) (@nil (Field.K (K p)))) *)
induction n as [| n IH]; intros [|i]; simpl; auto.
Qed.

Lemma proj_e n i j : j < n ->
  proj n i ('e_j) = if (i ?= j)%nat then 1%f else 0%f.
Proof.
(* Goal: forall (_ : lt i n) (_ : lt j n), @Logic.eq (Field.K (K p)) (pscal n (gen n i : kn n) (gen n j)) (if eq_nat i j then v1 (K p) else v0 (K p)) *)
generalize i j; clear i j.
induction n as [| n IH]; intros [|i] [|j] H; 
  simpl; auto with arith; try (contradict H; auto with arith; fail).
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
rewrite proj0; auto.
Qed.

Lemma proj_scal n i k x :  proj n i (k .* x) = (k * proj n i x)%f.
Proof.
(* Goal: @Logic.eq (Field.K (K p)) (proj n i (scalE (vn_eparams n) k x)) (multK (stype (vn_eparams n)) k (proj n i x)) *)
generalize i x; clear i x.
(* Goal: @Logic.eq (kn n) (kprod n (kprod n a b) c) (kprod n a (kprod n b c)) *)
induction n as [| n IH]; simpl; auto.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
Krm0.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
intros [| i] [x1 x2]; auto.
(* Goal: @Logic.eq (Field.K (K p)) (proj n i (scal n k x2)) (multK (K p) k (proj n i x2)) *)
exact (IH _ i x2).
Qed.

Lemma proj_add n i x y : 
 proj n i (x + y) = (proj n i x + proj n i y)%f.
Proof.
generalize  i x y; clear i x y.
(* Goal: @Logic.eq (kn n) (kprod n (kprod n a b) c) (kprod n a (kprod n b c)) *)
induction n as [| n IH]; simpl; auto.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
intros [| i]; Krm0.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
intros [| i] (x1,x2) (x3,x4); auto.
(* Goal: @Logic.eq (Field.K (K p)) (proj n i (add n x2 x4)) (addK (K p) (proj n i x2) (proj n i x4)) *)
exact (IH i x2 x4).
Qed.

Fixpoint pscal (n: nat): (kn n) -> (kn n) -> K :=
  match n return kn n -> kn n -> K with 
  | O => fun a b => 0%f
  | S n1 => fun l1 l2 => let (a,l3) := l1 in let (b,l4) := l2 in
                         (a * b + pscal n1 l3 l4)%f
  end.

Notation "a  [.]  b" := (pscal _ a b) (at level 40): kn_scope.

Lemma pscal0l n (x: kn n) : 0 [.] x = 0%f.
Proof.
(* Goal: @Logic.eq (Field.K (K p)) (pscal n x y) (pscal n y x) *)
induction n as [| n IH]; simpl.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
 intros; Krm0.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
destruct x; rewrite IH; Krm0.
Qed.

Lemma pscal0r n (x: kn n) : x [.] 0 = 0%f.
Proof.
(* Goal: @Logic.eq (Field.K (K p)) (pscal n x y) (pscal n y x) *)
induction n as [| n IH]; simpl.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
 intros; Krm0.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
destruct x; rewrite IH; Krm0.
Qed.

Lemma pscal_com n (x y: kn n) : x [.] y = y [.] x.
Proof.
(* Goal: @Logic.eq (Field.K (K p)) (pscal n x y) (pscal n y x) *)
induction n as [| n IH]; simpl.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
 intros; Krm0.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
destruct x; destruct y; rewrite multK_com, IH; auto.
Qed.

Lemma pscal_e n (i j: nat) : i < n -> j < n ->
  ('e_i: kn n) [.] ('e_j) = if (i ?= j)%nat then 1%f else 0%f.
Proof.
(* Goal: forall (_ : lt i n) (_ : lt j n), @Logic.eq (Field.K (K p)) (pscal n (gen n i : kn n) (gen n j)) (if eq_nat i j then v1 (K p) else v0 (K p)) *)
generalize i j; clear i j.
(* Goal: forall (i j : nat) (_ : lt i n) (_ : lt j n), @Logic.eq (Field.K (K p)) (pscal n (gen n i) (gen n j)) (if eq_nat i j then v1 (K p) else v0 (K p)) *)
induction n as [| n IH].
(* Goal: forall (i j : nat) (_ : lt i O) (_ : lt j O), @Logic.eq (Field.K (K p)) (pscal O (gen O i) (gen O j)) (if eq_nat i j then v1 (K p) else v0 (K p)) *)
(* Goal: forall (i j : nat) (_ : lt i (S n)) (_ : lt j (S n)), @Logic.eq (Field.K (K p)) (pscal (S n) (gen (S n) i) (gen (S n) j)) (if eq_nat i j then v1 (K p) else v0 (K p)) *)
  intros i j HH; contradict HH; auto with arith.
intros [|i] [|j] Hi Hj; 
  simpl; auto with arith; 
  try rewrite pscal0l; try rewrite pscal0r; Krm0; Krm1.
(* Goal: @Logic.eq (Field.K (K p)) (pscal n (gen n i) (gen n j)) (if eq_nat i j then v1 (K p) else v0 (K p)) *)
apply IH; auto with arith.
Qed.

Lemma pscal_scall n k (x y: kn n) :  
  (k .* x) [.] y = (k * (x [.] y))%f.
Proof.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
induction n as [| n IH]; simpl; auto; try Kfold n; Krm0.
(* Goal: @Logic.eq (Field.K (K p)) (let (a, l3) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scalE (vn_eparams n) k l2) in let (b, l4) := y in addK (K p) (multK (K p) a b) (pscal n l3 l4)) (multK (K p) k (let (a, l3) := x in let (b, l4) := y in addK (K p) (multK (K p) a b) (pscal n l3 l4))) *)
destruct x; destruct y.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
rewrite add_multKr, multK_assoc, IH; auto.
Qed.

Lemma pscal_scalr n k (x y: kn n) :  
  x [.] (k .* y) = (k * (x [.] y))%f.
Proof.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
induction n as [| n IH]; simpl; auto; try Kfold n; Krm0.
(* Goal: @Logic.eq (Field.K (K p)) (let (a, l3) := x in let (b, l4) := let (v1, l2) := y in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scalE (vn_eparams n) k l2) in addK (K p) (multK (K p) a b) (pscal n l3 l4)) (multK (K p) k (let (a, l3) := x in let (b, l4) := y in addK (K p) (multK (K p) a b) (pscal n l3 l4))) *)
destruct x as [a x]; destruct y.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
rewrite add_multKr, <-multK_assoc, (multK_com _ Hp a), multK_assoc, IH; auto.
Qed.

Lemma pscal_addl n (x y z: kn n) :  
  (x + y) [.] z = (x [.] z + (y [.] z))%f.
Proof.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
induction n as [| n IH]; simpl; auto; try Kfold n; Krm0.
(* Goal: @Logic.eq (Field.K (K p)) (let (a, l3) := z in let (b, l4) := let (v1, l4) := x in let (v2, l5) := y in @pair (Field.K (K p)) (kn n) (addK (K p) v1 v2) (addE (vn_eparams n) l4 l5) in addK (K p) (multK (K p) a b) (pscal n l3 l4)) (addK (K p) (let (a, l3) := z in let (b, l4) := x in addK (K p) (multK (K p) a b) (pscal n l3 l4)) (let (a, l3) := z in let (b, l4) := y in addK (K p) (multK (K p) a b) (pscal n l3 l4))) *)
destruct x; destruct y as [b y]; destruct z as [c z].
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
rewrite add_multKl, IH; auto.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
rewrite !addK_assoc; auto.
rewrite <-(addK_assoc _ Hp (b * c)%f), (addK_com _ Hp (b * c)%f),
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
        !addK_assoc; auto.
Qed.

Lemma pscal_addr n (x y z: kn n) :  
  z [.] (x + y) = (z [.] x + (z [.] y))%f.
Proof.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
induction n as [| n IH]; simpl; auto; try Kfold n; Krm0.
(* Goal: @Logic.eq (Field.K (K p)) (let (a, l3) := z in let (b, l4) := let (v1, l4) := x in let (v2, l5) := y in @pair (Field.K (K p)) (kn n) (addK (K p) v1 v2) (addE (vn_eparams n) l4 l5) in addK (K p) (multK (K p) a b) (pscal n l3 l4)) (addK (K p) (let (a, l3) := z in let (b, l4) := x in addK (K p) (multK (K p) a b) (pscal n l3 l4)) (let (a, l3) := z in let (b, l4) := y in addK (K p) (multK (K p) a b) (pscal n l3 l4))) *)
destruct x; destruct y as [b y]; destruct z as [c z].
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
rewrite add_multKr, IH; auto.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
rewrite !addK_assoc; auto.
rewrite <-(addK_assoc _ Hp (c * b)%f), (addK_com _ Hp (c * b)%f),
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
        !addK_assoc; auto.
Qed.

(* Our final vector *)
Definition Kn := kn p.
Definition K0 := genk p 0%f.
Definition Keq: Kn -> Kn -> bool := eq p.
Definition Kadd: Kn -> Kn -> Kn := add p.
Definition Kscal: K -> Kn -> Kn := scal p.
Definition Kproj: nat -> Kn -> K := proj p.
Definition Ksprod: Kn -> Kn -> K := pscal p.
Definition Kgen := gen p.

Canonical Structure v_eparams :=
  Build_eparams Kn K K0 Keq Kadd Kscal.
Definition f : vparamsProp v_eparams := fn p.

(* Prod of two vectors as list *)
Fixpoint kprod (n : nat) : kn n -> kn n -> kn n :=
  match n with
  | 0%nat => fun a b => tt
  | S n1 =>
      fun l1 l2 =>
      let (v1, l3) := l1 in
      let (v2, l4) := l2 in ((v1 * v2)%f, kprod n1 l3 l4)
  end.

Local Notation "a  [*]  b" := (kprod _ a b) (at level 40).

Lemma kprod0l n a : 0 [*] a = 0 :> kn n.
Proof.
(* Goal: eql_t0 (kn2l (S n) (gen (S n) O)) (@cons (Field.K (K p)) (v1 (K p)) (@nil (Field.K (K p)))) *)
induction n as [|n IH]; simpl; auto.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
destruct a; simpl; rewrite IH; Krm0.
Qed.

Lemma kprod0r n a : a [*] 0 = 0 :> kn n.
Proof.
(* Goal: eql_t0 (kn2l (S n) (gen (S n) O)) (@cons (Field.K (K p)) (v1 (K p)) (@nil (Field.K (K p)))) *)
induction n as [|n IH]; simpl; auto.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
destruct a; simpl; rewrite IH; Krm0.
Qed.

Lemma kprodkl n k a : [k] [*] a = k .* a :> kn n.
Proof.
(* Goal: eql_t0 (kn2l (S n) (gen (S n) O)) (@cons (Field.K (K p)) (v1 (K p)) (@nil (Field.K (K p)))) *)
induction n as [|n IH]; destruct a; simpl; auto.
(* Goal: @Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) (multK (K p) k k0) (kprod n (genk n k) k1)) (@pair (Field.K (K p)) (kn n) (multK (K p) k k0) (scal n k k1)) *)
rewrite IH; Krm1.
Qed.

Lemma kprodkr n k a : a [*] [k] = k .* a :> kn n.
Proof.
(* Goal: eql_t0 (kn2l (S n) (gen (S n) O)) (@cons (Field.K (K p)) (v1 (K p)) (@nil (Field.K (K p)))) *)
induction n as [|n IH]; destruct a; simpl; auto.
(* Goal: @Logic.eq (prod (Field.K (K p)) (kn n)) (@pair (Field.K (K p)) (kn n) (multK (K p) k0 k) (kprod n k1 (genk n k))) (@pair (Field.K (K p)) (kn n) (multK (K p) k k0) (scal n k k1)) *)
rewrite IH, multK_com; Krm1.
Qed.

Lemma kprod1l n a : [1%f] [*] a = a :> kn n.
Proof.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
rewrite kprodkl, scalE1; auto.
Qed.

Lemma kprod1r n a : a [*] [1%f] = a :> kn n.
Proof.
(* Goal: forall n i : nat, @Logic.eq (kn (S n)) (gen (S n) (S i)) (lift n (gen n i)) *)
rewrite kprodkr, scalE1; auto.
Qed.

Lemma kprod_addl n a b c : 
  (a + b) [*] c = a [*] c + b [*] c :> kn n.
Proof.
(* Goal: eql_t0 (kn2l (S n) (gen (S n) O)) (@cons (Field.K (K p)) (v1 (K p)) (@nil (Field.K (K p)))) *)
induction n as [|n IH]; simpl; auto.
(* Goal: forall (_ : @Logic.eq (E (vn_eparams (S n))) (addE (vn_eparams (S n)) (scalE (vn_eparams (S n)) k (@pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p))))) (lift n (mprod (vn_eparams n) ks (base n)))) (E0 (vn_eparams (S n)))) (k0 : Field.K (stype (vn_eparams (S n)))) (_ : @In (Field.K (stype (vn_eparams (S n)))) k0 (@cons (Field.K (stype (vn_eparams (S n)))) k ks)), @Logic.eq (Field.K (stype (vn_eparams (S n)))) k0 (v0 (stype (vn_eparams (S n)))) *)
destruct a; destruct b; destruct c; simpl.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
Kfold n; rewrite IH, add_multKl; Krm0.
Qed.

Lemma kprod_addr n a b c : 
  a [*] (b + c) = a [*] b + a [*] c :> kn n.
Proof.
(* Goal: eql_t0 (kn2l (S n) (gen (S n) O)) (@cons (Field.K (K p)) (v1 (K p)) (@nil (Field.K (K p)))) *)
induction n as [|n IH]; simpl; auto.
(* Goal: forall (_ : @Logic.eq (E (vn_eparams (S n))) (addE (vn_eparams (S n)) (scalE (vn_eparams (S n)) k (@pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p))))) (lift n (mprod (vn_eparams n) ks (base n)))) (E0 (vn_eparams (S n)))) (k0 : Field.K (stype (vn_eparams (S n)))) (_ : @In (Field.K (stype (vn_eparams (S n)))) k0 (@cons (Field.K (stype (vn_eparams (S n)))) k ks)), @Logic.eq (Field.K (stype (vn_eparams (S n)))) k0 (v0 (stype (vn_eparams (S n)))) *)
destruct a; destruct b; destruct c; simpl.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
Kfold n; rewrite IH, add_multKr; Krm0.
Qed.

Lemma kprod_scall n k a b : 
  (k .* a) [*] b = k .* (a [*] b) :> kn n.
Proof.
(* Goal: eql_t0 (kn2l (S n) (gen (S n) O)) (@cons (Field.K (K p)) (v1 (K p)) (@nil (Field.K (K p)))) *)
induction n as [|n IH]; simpl; auto.
(* Goal: forall (_ : @Logic.eq (E (vn_eparams (S n))) (addE (vn_eparams (S n)) (scalE (vn_eparams (S n)) k (@pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p))))) (lift n (mprod (vn_eparams n) ks (base n)))) (E0 (vn_eparams (S n)))) (k0 : Field.K (stype (vn_eparams (S n)))) (_ : @In (Field.K (stype (vn_eparams (S n)))) k0 (@cons (Field.K (stype (vn_eparams (S n)))) k ks)), @Logic.eq (Field.K (stype (vn_eparams (S n)))) k0 (v0 (stype (vn_eparams (S n)))) *)
destruct a; destruct b; simpl.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
Kfold n; rewrite IH, multK_assoc; Krm0.
Qed.

Lemma kprod_scalr n k a b : 
  a [*] (k .* b) = k .* (a [*] b) :> kn n.
Proof.
(* Goal: eql_t0 (kn2l (S n) (gen (S n) O)) (@cons (Field.K (K p)) (v1 (K p)) (@nil (Field.K (K p)))) *)
induction n as [|n IH]; simpl; auto.
(* Goal: forall (_ : @Logic.eq (E (vn_eparams (S n))) (addE (vn_eparams (S n)) (scalE (vn_eparams (S n)) k (@pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p))))) (lift n (mprod (vn_eparams n) ks (base n)))) (E0 (vn_eparams (S n)))) (k0 : Field.K (stype (vn_eparams (S n)))) (_ : @In (Field.K (stype (vn_eparams (S n)))) k0 (@cons (Field.K (stype (vn_eparams (S n)))) k ks)), @Logic.eq (Field.K (stype (vn_eparams (S n)))) k0 (v0 (stype (vn_eparams (S n)))) *)
destruct a; destruct b; simpl.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
Kfold n; rewrite IH, multK_swap; Krm0.
Qed.

Lemma kprod_assoc n a b c : 
  (a [*] b) [*] c = a [*] (b [*] c) :> kn n.
Proof.
(* Goal: eql_t0 (kn2l (S n) (gen (S n) O)) (@cons (Field.K (K p)) (v1 (K p)) (@nil (Field.K (K p)))) *)
induction n as [|n IH]; simpl; auto.
(* Goal: forall (_ : @Logic.eq (E (vn_eparams (S n))) (addE (vn_eparams (S n)) (scalE (vn_eparams (S n)) k (@pair (Field.K (K p)) (kn n) (v1 (K p)) (genk n (v0 (K p))))) (lift n (mprod (vn_eparams n) ks (base n)))) (E0 (vn_eparams (S n)))) (k0 : Field.K (stype (vn_eparams (S n)))) (_ : @In (Field.K (stype (vn_eparams (S n)))) k0 (@cons (Field.K (stype (vn_eparams (S n)))) k ks)), @Logic.eq (Field.K (stype (vn_eparams (S n)))) k0 (v0 (stype (vn_eparams (S n)))) *)
destruct a; destruct b; destruct c; simpl.
(* Goal: forall (_ : nat) (_ : unit), @Logic.eq (Field.K (K p)) (v0 (K p)) (multK (K p) k (v0 (K p))) *)
(* Goal: forall (i : nat) (x : prod (Field.K (K p)) (kn n)), @Logic.eq (Field.K (K p)) (let (a, l1) := let (v1, l2) := x in @pair (Field.K (K p)) (kn n) (multK (K p) k v1) (scal n k l2) in match i with | O => a | S k1 => proj n k1 l1 end) (multK (K p) k (let (a, l1) := x in match i with | O => a | S k1 => proj n k1 l1 end)) *)
Kfold n; rewrite IH, multK_assoc; Krm0.
Qed.

End Kn.

Notation " 'e_ p" := (gen _ _ p) (at level 8) : Kn_scope.
Notation " [ k ] " := (genk _ _ k) (at level 9) : Kn_scope.
Notation "a  [.]  b" := (pscal _ _ a b) (at level 40): Kn_scope.
Notation "a  [*]  b" := (kprod _ _ a b) (at level 40): Kn_scope.

Delimit Scope Kn_scope with Kn.

Hint Constructors eql_t0.
