Require Import Basics.Overture Basics.Decidable Spaces.Nat.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Algebra.Rings.Ring.
Require Import Classes.interfaces.abstract_algebra.

Local Set Universe Minimization ToSet.
Local Set Polymorphic Inductive Cumulativity.

(** ** Kronecker Delta *)

Section AssumeDecidable.
  (** Throughout this section, we assume that we have a type [A] with decidable equality. This will be our indexing type and can be thought of as [nat] for reading purposes. *)

  Universes u v.
  Context {A : Type@{u}} `{DecidablePaths@{u} A} {R : Ring@{v}}.

  (** The Kronecker delta function is a function of elements of [A] that is 1 when the two numbers are equal and 0 otherwise. It is useful for working with finite sums of ring elements. *)
  Definition kronecker_delta@{} (i j : A) : R
    := if dec (i = j) then 1 else 0.

  (** Kronecker delta with the same index is 1. *)
  Definition kronecker_delta_refl@{} (i : A)
    : kronecker_delta i i = 1.
A: Type
H: DecidablePaths A
R: Ring
i: A
kronecker_delta i i = 1
  Proof.
A: Type
H: DecidablePaths A
R: Ring
i: A
kronecker_delta i i = 1
    unfold kronecker_delta.
A: Type
H: DecidablePaths A
R: Ring
i: A
(if dec (i = i) then 1 else 0) = 1
    generalize (dec (i = i)).
A: Type
H: DecidablePaths A
R: Ring
i: A
forall s : (i = i) + (i <> i),
(if s then 1 else 0) = 1
    by rapply decidable_paths_refl.
  Defined.

  (** Kronecker delta with differing indices is 0. *)
  Definition kronecker_delta_neq@{} {i j : A} (p : i <> j)
    : kronecker_delta i j = 0.
A: Type
H: DecidablePaths A
R: Ring
i, j: A
p: i <> j
kronecker_delta i j = 0
  Proof.
A: Type
H: DecidablePaths A
R: Ring
i, j: A
p: i <> j
kronecker_delta i j = 0
    unfold kronecker_delta.
A: Type
H: DecidablePaths A
R: Ring
i, j: A
p: i <> j
(if dec (i = j) then 1 else 0) = 0
    by decidable_false (dec (i = j)) p.
  Defined.

  (** Kronecker delta is symmetric in its arguments. *)
  Definition kronecker_delta_symm@{} (i j : A)
    : kronecker_delta i j = kronecker_delta j i.
A: Type
H: DecidablePaths A
R: Ring
i, j: A
kronecker_delta i j = kronecker_delta j i
  Proof.
A: Type
H: DecidablePaths A
R: Ring
i, j: A
kronecker_delta i j = kronecker_delta j i
    unfold kronecker_delta.
A: Type
H: DecidablePaths A
R: Ring
i, j: A
(if dec (i = j) then 1 else 0) =
(if dec (j = i) then 1 else 0)
    destruct (dec (i = j)) as [p|q].
A: Type
H: DecidablePaths A
R: Ring
i, j: A
p: i = j
1 = (if dec (j = i) then 1 else 0)
A: Type
H: DecidablePaths A
R: Ring
i, j: A
q: i <> j
0 = (if dec (j = i) then 1 else 0)
    -
A: Type
H: DecidablePaths A
R: Ring
i, j: A
p: i = j
1 = (if dec (j = i) then 1 else 0) by decidable_true (dec (j = i)) p^.
    -
A: Type
H: DecidablePaths A
R: Ring
i, j: A
q: i <> j
0 = (if dec (j = i) then 1 else 0) by decidable_false (dec (j = i)) (symmetric_neq q).
  Defined.

  (** An injective endofunction on [A] preserves the Kronecker delta. *)
  Definition kronecker_delta_map_inj@{} (i j : A) (f : A -> A)
    `{!IsInjective f}
    : kronecker_delta (f i) (f j) = kronecker_delta i j.
A: Type
H: DecidablePaths A
R: Ring
i, j: A
f: A -> A
IsInjective0: IsInjective f
kronecker_delta (f i) (f j) = kronecker_delta i j
  Proof.
A: Type
H: DecidablePaths A
R: Ring
i, j: A
f: A -> A
IsInjective0: IsInjective f
kronecker_delta (f i) (f j) = kronecker_delta i j
    unfold kronecker_delta.
A: Type
H: DecidablePaths A
R: Ring
i, j: A
f: A -> A
IsInjective0: IsInjective f
(if dec (f i = f j) then 1 else 0) =
(if dec (i = j) then 1 else 0)
    destruct (dec (i = j)) as [p|p].
A: Type
H: DecidablePaths A
R: Ring
i, j: A
f: A -> A
IsInjective0: IsInjective f
p: i = j
(if dec (f i = f j) then 1 else 0) = 1
A: Type
H: DecidablePaths A
R: Ring
i, j: A
f: A -> A
IsInjective0: IsInjective f
p: i <> j
(if dec (f i = f j) then 1 else 0) = 0
    -
A: Type
H: DecidablePaths A
R: Ring
i, j: A
f: A -> A
IsInjective0: IsInjective f
p: i = j
(if dec (f i = f j) then 1 else 0) = 1 by decidable_true (dec (f i = f j)) (ap f p).
    -
A: Type
H: DecidablePaths A
R: Ring
i, j: A
f: A -> A
IsInjective0: IsInjective f
p: i <> j
(if dec (f i = f j) then 1 else 0) = 0 destruct (dec (f i = f j)) as [q|q].
A: Type
H: DecidablePaths A
R: Ring
i, j: A
f: A -> A
IsInjective0: IsInjective f
p: i <> j
q: f i = f j
1 = 0
A: Type
H: DecidablePaths A
R: Ring
i, j: A
f: A -> A
IsInjective0: IsInjective f
p: i <> j
q: f i <> f j
0 = 0
      +
A: Type
H: DecidablePaths A
R: Ring
i, j: A
f: A -> A
IsInjective0: IsInjective f
p: i <> j
q: f i = f j
1 = 0 apply (injective f) in q.
A: Type
H: DecidablePaths A
R: Ring
i, j: A
f: A -> A
IsInjective0: IsInjective f
p: i <> j
q: i = j
1 = 0
        contradiction.
      +
A: Type
H: DecidablePaths A
R: Ring
i, j: A
f: A -> A
IsInjective0: IsInjective f
p: i <> j
q: f i <> f j
0 = 0 reflexivity.
  Defined.

  (** Kronecker delta commutes with any ring element. *)
  Definition kronecker_delta_comm@{} (i j : A) (r : R)
    : r * kronecker_delta i j = kronecker_delta i j * r.
A: Type
H: DecidablePaths A
R: Ring
i, j: A
r: R
r * kronecker_delta i j = kronecker_delta i j * r
  Proof.
A: Type
H: DecidablePaths A
R: Ring
i, j: A
r: R
r * kronecker_delta i j = kronecker_delta i j * r
    unfold kronecker_delta.
A: Type
H: DecidablePaths A
R: Ring
i, j: A
r: R
r * (if dec (i = j) then 1 else 0) =
(if dec (i = j) then 1 else 0) * r
    destruct (dec (i = j)).
A: Type
H: DecidablePaths A
R: Ring
i, j: A
r: R
p: i = j
r * 1 = 1 * r
A: Type
H: DecidablePaths A
R: Ring
i, j: A
r: R
n: i <> j
r * 0 = 0 * r
    -
A: Type
H: DecidablePaths A
R: Ring
i, j: A
r: R
p: i = j
r * 1 = 1 * r exact (rng_mult_one_r _ @ (rng_mult_one_l _)^).
    -
A: Type
H: DecidablePaths A
R: Ring
i, j: A
r: R
n: i <> j
r * 0 = 0 * r exact (rng_mult_zero_r _ @ (rng_mult_zero_l _)^).
  Defined.

End AssumeDecidable.

(** The following lemmas are specialised to when the indexing type is [nat]. *)

(** Kronecker delta where the first index is strictly less than the second is 0. *)
Definition kronecker_delta_lt {R : Ring} {i j : nat} (p : (i < j)%nat)
  : kronecker_delta (R:=R) i j = 0.
R: Ring
i, j: nat
p: (i < j)%nat
kronecker_delta i j = 0
Proof.
R: Ring
i, j: nat
p: (i < j)%nat
kronecker_delta i j = 0
  apply kronecker_delta_neq.
R: Ring
i, j: nat
p: (i < j)%nat
i <> j
  intros q; destruct q.
R: Ring
i: nat
p: (i < i)%nat
Empty
  by apply lt_irrefl in p.
Defined.

(** Kronecker delta where the first index is strictly greater than the second is 0. *)
Definition kronecker_delta_gt {R : Ring} {i j : nat} (p : (j < i)%nat)
  : kronecker_delta (R:=R) i j = 0.
R: Ring
i, j: nat
p: (j < i)%nat
kronecker_delta i j = 0
Proof.
R: Ring
i, j: nat
p: (j < i)%nat
kronecker_delta i j = 0
  apply kronecker_delta_neq.
R: Ring
i, j: nat
p: (j < i)%nat
i <> j
  intros q; destruct q.
R: Ring
i: nat
p: (i < i)%nat
Empty
  by apply lt_irrefl in p.
Defined.

(** Kronecker delta can be used to extract a single term from a finite sum. *)
Definition rng_sum_kronecker_delta_l {R : Ring} (n i : nat) (Hi : (i < n)%nat)
  (f : forall k, (k < n)%nat -> R)
  : ab_sum n (fun j Hj => kronecker_delta i j * f j Hj) = f i Hi.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
ab_sum n
  (fun (j : nat) (Hj : (j < n)%nat) =>
   kronecker_delta i j * f j Hj) = f i Hi
Proof.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
ab_sum n
  (fun (j : nat) (Hj : (j < n)%nat) =>
   kronecker_delta i j * f j Hj) = f i Hi
  revert i Hi f; simple_induction n n IHn; intros i Hi f.
R: Ring
i: nat
Hi: (i < 0)%nat
f: forall k : nat, (k < 0)%nat -> R
ab_sum 0
  (fun (j : nat) (Hj : (j < 0)%nat) =>
   kronecker_delta i j * f j Hj) = f i Hi
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
ab_sum n.+1
  (fun (j : nat) (Hj : (j < n.+1)%nat) =>
   kronecker_delta i j * f j Hj) = f i Hi
  1: destruct (not_lt_zero_r _ Hi).
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
ab_sum n.+1
  (fun (j : nat) (Hj : (j < n.+1)%nat) =>
   kronecker_delta i j * f j Hj) = f i Hi
  destruct (dec (i = n)) as [p|p].
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
p: i = n
ab_sum n.+1
  (fun (j : nat) (Hj : (j < n.+1)%nat) =>
   kronecker_delta i j * f j Hj) = f i Hi
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
p: i <> n
ab_sum n.+1
  (fun (j : nat) (Hj : (j < n.+1)%nat) =>
   kronecker_delta i j * f j Hj) = f i Hi
  -
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
p: i = n
ab_sum n.+1
  (fun (j : nat) (Hj : (j < n.+1)%nat) =>
   kronecker_delta i j * f j Hj) = f i Hi destruct p; simpl.
R: Ring
i: nat
Hi: (i < i.+1)%nat
f: forall k : nat, (k < i.+1)%nat -> R
IHn: forall (i0 : nat) (Hi : (i0 < i)%nat) (f : forall k : nat, (k < i)%nat -> R),
ab_sum i (fun (j : nat) (Hj : (j < i)%nat) => kronecker_delta i0 j * f j Hj) =
f i0 Hi
sg_op (kronecker_delta i i * f i (leq_refl i.+1))
  (ab_sum i
     (fun (k : nat) (Hk : (k < i)%nat) =>
      kronecker_delta i k * f k (leq_succ_r Hk))) =
f i Hi
    rewrite kronecker_delta_refl.
R: Ring
i: nat
Hi: (i < i.+1)%nat
f: forall k : nat, (k < i.+1)%nat -> R
IHn: forall (i0 : nat) (Hi : (i0 < i)%nat) (f : forall k : nat, (k < i)%nat -> R),
ab_sum i (fun (j : nat) (Hj : (j < i)%nat) => kronecker_delta i0 j * f j Hj) =
f i0 Hi
sg_op (1 * f i (leq_refl i.+1))
  (ab_sum i
     (fun (k : nat) (Hk : (k < i)%nat) =>
      kronecker_delta i k * f k (leq_succ_r Hk))) =
f i Hi
    rewrite rng_mult_one_l.
R: Ring
i: nat
Hi: (i < i.+1)%nat
f: forall k : nat, (k < i.+1)%nat -> R
IHn: forall (i0 : nat) (Hi : (i0 < i)%nat) (f : forall k : nat, (k < i)%nat -> R),
ab_sum i (fun (j : nat) (Hj : (j < i)%nat) => kronecker_delta i0 j * f j Hj) =
f i0 Hi
sg_op (f i (leq_refl i.+1))
  (ab_sum i
     (fun (k : nat) (Hk : (k < i)%nat) =>
      kronecker_delta i k * f k (leq_succ_r Hk))) =
f i Hi
    rewrite <- rng_plus_zero_r.
R: Ring
i: nat
Hi: (i < i.+1)%nat
f: forall k : nat, (k < i.+1)%nat -> R
IHn: forall (i0 : nat) (Hi : (i0 < i)%nat) (f : forall k : nat, (k < i)%nat -> R),
ab_sum i (fun (j : nat) (Hj : (j < i)%nat) => kronecker_delta i0 j * f j Hj) =
f i0 Hi
sg_op (f i (leq_refl i.+1))
  (ab_sum i
     (fun (k : nat) (Hk : (k < i)%nat) =>
      kronecker_delta i k * f k (leq_succ_r Hk))) =
f i Hi + 0
    apply ap11.
R: Ring
i: nat
Hi: (i < i.+1)%nat
f: forall k : nat, (k < i.+1)%nat -> R
IHn: forall (i0 : nat) (Hi : (i0 < i)%nat) (f : forall k : nat, (k < i)%nat -> R),
ab_sum i (fun (j : nat) (Hj : (j < i)%nat) => kronecker_delta i0 j * f j Hj) =
f i0 Hi
sg_op (f i (leq_refl i.+1)) = plus (f i Hi)
R: Ring
i: nat
Hi: (i < i.+1)%nat
f: forall k : nat, (k < i.+1)%nat -> R
IHn: forall (i0 : nat) (Hi : (i0 < i)%nat) (f : forall k : nat, (k < i)%nat -> R),
ab_sum i (fun (j : nat) (Hj : (j < i)%nat) => kronecker_delta i0 j * f j Hj) =
f i0 Hi
ab_sum i
  (fun (k : nat) (Hk : (k < i)%nat) =>
   kronecker_delta i k * f k (leq_succ_r Hk)) = 0
    {
R: Ring
i: nat
Hi: (i < i.+1)%nat
f: forall k : nat, (k < i.+1)%nat -> R
IHn: forall (i0 : nat) (Hi : (i0 < i)%nat) (f : forall k : nat, (k < i)%nat -> R),
ab_sum i (fun (j : nat) (Hj : (j < i)%nat) => kronecker_delta i0 j * f j Hj) =
f i0 Hi
sg_op (f i (leq_refl i.+1)) = plus (f i Hi) apply (ap (fun h => plus (f i h))), path_ishprop. }
R: Ring
i: nat
Hi: (i < i.+1)%nat
f: forall k : nat, (k < i.+1)%nat -> R
IHn: forall (i0 : nat) (Hi : (i0 < i)%nat) (f : forall k : nat, (k < i)%nat -> R),
ab_sum i (fun (j : nat) (Hj : (j < i)%nat) => kronecker_delta i0 j * f j Hj) =
f i0 Hi
ab_sum i
  (fun (k : nat) (Hk : (k < i)%nat) =>
   kronecker_delta i k * f k (leq_succ_r Hk)) = 0
    napply ab_sum_zero.
R: Ring
i: nat
Hi: (i < i.+1)%nat
f: forall k : nat, (k < i.+1)%nat -> R
IHn: forall (i0 : nat) (Hi : (i0 < i)%nat) (f : forall k : nat, (k < i)%nat -> R),
ab_sum i (fun (j : nat) (Hj : (j < i)%nat) => kronecker_delta i0 j * f j Hj) =
f i0 Hi
forall (k : nat) (Hk : (k < i)%nat),
kronecker_delta i k * f k (leq_succ_r Hk) = mon_unit
    intros k Hk.
R: Ring
i: nat
Hi: (i < i.+1)%nat
f: forall k : nat, (k < i.+1)%nat -> R
IHn: forall (i0 : nat) (Hi : (i0 < i)%nat) (f : forall k : nat, (k < i)%nat -> R),
ab_sum i (fun (j : nat) (Hj : (j < i)%nat) => kronecker_delta i0 j * f j Hj) =
f i0 Hi
k: nat
Hk: (k < i)%nat
kronecker_delta i k * f k (leq_succ_r Hk) = mon_unit
    rewrite (kronecker_delta_gt Hk).
R: Ring
i: nat
Hi: (i < i.+1)%nat
f: forall k : nat, (k < i.+1)%nat -> R
IHn: forall (i0 : nat) (Hi : (i0 < i)%nat) (f : forall k : nat, (k < i)%nat -> R),
ab_sum i (fun (j : nat) (Hj : (j < i)%nat) => kronecker_delta i0 j * f j Hj) =
f i0 Hi
k: nat
Hk: (k < i)%nat
0 * f k (leq_succ_r Hk) = mon_unit
    apply rng_mult_zero_l.
  -
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
p: i <> n
ab_sum n.+1
  (fun (j : nat) (Hj : (j < n.+1)%nat) =>
   kronecker_delta i j * f j Hj) = f i Hi simpl; lhs napply ap.
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
p: i <> n
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   kronecker_delta i k * f k (leq_succ_r Hk)) = ?Goal
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
p: i <> n
sg_op (kronecker_delta i n * f n (leq_refl n.+1))
  ?Goal = f i Hi
    +
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
p: i <> n
ab_sum n
  (fun (k : nat) (Hk : (k < n)%nat) =>
   kronecker_delta i k * f k (leq_succ_r Hk)) = ?Goal napply IHn.
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
p: i <> n
(i < n)%nat
      apply neq_iff_lt_or_gt in p.
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
p: ((i < n)%nat + (i > n)%nat)%type
(i < n)%nat
      destruct p; [assumption|].
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
g: (i > n)%nat
(i < n)%nat
      apply gt_iff_not_leq in Hi.
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: ~ (n.+1 <= i)%nat
f: forall k : nat, (k < n.+1)%nat -> R
g: (i > n)%nat
(i < n)%nat
      contradiction Hi.
    +
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
p: i <> n
sg_op (kronecker_delta i n * f n (leq_refl n.+1))
  (f i
     (leq_succ_r
        (let H := fst neq_iff_lt_or_gt in
         let p := H p in
         match p with
         | inl l => idmap l
         | inr g =>
             (fun g0 : (i > n)%nat =>
              let H0 := snd gt_iff_not_leq in
              let Hi := H0 Hi in
              Overture.Empty_rec (i < n)%nat (Hi g0))
               g
         end))) = f i Hi rewrite (kronecker_delta_neq p).
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
p: i <> n
sg_op (0 * f n (leq_refl n.+1))
  (f i
     (leq_succ_r
        (let H := fst neq_iff_lt_or_gt in
         let p := H p in
         match p with
         | inl l => l
         | inr g =>
             let H0 := snd gt_iff_not_leq in
             let Hi := H0 Hi in
             Overture.Empty_rec (i < n)%nat (Hi g)
         end))) = f i Hi
      rewrite rng_mult_zero_l.
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
p: i <> n
sg_op 0
  (f i
     (leq_succ_r
        (let H := fst neq_iff_lt_or_gt in
         let p := H p in
         match p with
         | inl l => l
         | inr g =>
             let H0 := snd gt_iff_not_leq in
             let Hi := H0 Hi in
             Overture.Empty_rec (i < n)%nat (Hi g)
         end))) = f i Hi
      rewrite grp_unit_l.
R: Ring
n: nat
IHn: forall (i : nat) (Hi : (i < n)%nat) (f : forall k : nat, (k < n)%nat -> R),
ab_sum n (fun (j : nat) (Hj : (j < n)%nat) => kronecker_delta i j * f j Hj) =
f i Hi
i: nat
Hi: (i < n.+1)%nat
f: forall k : nat, (k < n.+1)%nat -> R
p: i <> n
f i
  (leq_succ_r
     (let H := fst neq_iff_lt_or_gt in
      let p := H p in
      match p with
      | inl l => l
      | inr g =>
          let H0 := snd gt_iff_not_leq in
          let Hi := H0 Hi in
          Overture.Empty_rec (i < n)%nat (Hi g)
      end)) = f i Hi
      apply ap, path_ishprop.
Defined.

(** Variant of [rng_sum_kronecker_delta_l] where the indexing is swapped. *)
Definition rng_sum_kronecker_delta_l' {R : Ring} (n i : nat) (Hi : (i < n)%nat)
  (f : forall k, (k < n)%nat -> R)
  : ab_sum n (fun j Hj => kronecker_delta j i * f j Hj) = f i Hi.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
ab_sum n
  (fun (j : nat) (Hj : (j < n)%nat) =>
   kronecker_delta j i * f j Hj) = f i Hi
Proof.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
ab_sum n
  (fun (j : nat) (Hj : (j < n)%nat) =>
   kronecker_delta j i * f j Hj) = f i Hi
  lhs napply path_ab_sum.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
forall (k : nat) (Hk : (k < n)%nat),
kronecker_delta k i * f k Hk = ?Goal k Hk
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
ab_sum n ?Goal = f i Hi
  2: napply rng_sum_kronecker_delta_l.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
forall (k : nat) (Hk : (k < n)%nat),
kronecker_delta k i * f k Hk =
(fun (j : nat) (Hj : (j < n)%nat) =>
 kronecker_delta i j * f j Hj) k Hk
  intros k Hk.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
k: nat
Hk: (k < n)%nat
kronecker_delta k i * f k Hk =
(fun (j : nat) (Hj : (j < n)%nat) =>
 kronecker_delta i j * f j Hj) k Hk
  cbn; f_ap; apply kronecker_delta_symm.
Defined.

(** Variant of [rng_sum_kronecker_delta_l] where the Kronecker delta appears on the right. *)
Definition rng_sum_kronecker_delta_r {R : Ring} (n i : nat) (Hi : (i < n)%nat)
  (f : forall k, (k < n)%nat -> R)
  : ab_sum n (fun j Hj => f j Hj * kronecker_delta i j) = f i Hi.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
ab_sum n
  (fun (j : nat) (Hj : (j < n)%nat) =>
   f j Hj * kronecker_delta i j) = f i Hi
Proof.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
ab_sum n
  (fun (j : nat) (Hj : (j < n)%nat) =>
   f j Hj * kronecker_delta i j) = f i Hi
  lhs napply path_ab_sum.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
forall (k : nat) (Hk : (k < n)%nat),
f k Hk * kronecker_delta i k = ?Goal k Hk
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
ab_sum n ?Goal = f i Hi
  2: napply rng_sum_kronecker_delta_l.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
forall (k : nat) (Hk : (k < n)%nat),
f k Hk * kronecker_delta i k =
(fun (j : nat) (Hj : (j < n)%nat) =>
 kronecker_delta i j * f j Hj) k Hk
  intros k Hk.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
k: nat
Hk: (k < n)%nat
f k Hk * kronecker_delta i k =
(fun (j : nat) (Hj : (j < n)%nat) =>
 kronecker_delta i j * f j Hj) k Hk
  apply kronecker_delta_comm.
Defined.

(** Variant of [rng_sum_kronecker_delta_r] where the indexing is swapped. *)
Definition rng_sum_kronecker_delta_r' {R : Ring} (n i : nat) (Hi : (i < n)%nat)
  (f : forall k, (k < n)%nat -> R)
  : ab_sum n (fun j Hj => f j Hj * kronecker_delta j i) = f i Hi.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
ab_sum n
  (fun (j : nat) (Hj : (j < n)%nat) =>
   f j Hj * kronecker_delta j i) = f i Hi
Proof.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
ab_sum n
  (fun (j : nat) (Hj : (j < n)%nat) =>
   f j Hj * kronecker_delta j i) = f i Hi
  lhs napply path_ab_sum.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
forall (k : nat) (Hk : (k < n)%nat),
f k Hk * kronecker_delta k i = ?Goal k Hk
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
ab_sum n ?Goal = f i Hi
  2: napply rng_sum_kronecker_delta_l'.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
forall (k : nat) (Hk : (k < n)%nat),
f k Hk * kronecker_delta k i =
(fun (j : nat) (Hj : (j < n)%nat) =>
 kronecker_delta j i * f j Hj) k Hk
  intros k Hk.
R: Ring
n, i: nat
Hi: (i < n)%nat
f: forall k : nat, (k < n)%nat -> R
k: nat
Hk: (k < n)%nat
f k Hk * kronecker_delta k i =
(fun (j : nat) (Hj : (j < n)%nat) =>
 kronecker_delta j i * f j Hj) k Hk
  apply kronecker_delta_comm.
Defined.