(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

(** ** Sparse ciphers *)

Require Import Arith Nat Omega List Bool Setoid.
Require Import utils_tac gcd sums rel_iter bool_nat power_decomp.

Set Implicit Arguments.

Local Notation power := (mscal mult 1).
Local Notation "∑" := (msum plus 0).
Local Infix "≲" := binary_le (at level 70, no associativity).
Local Infix "⇣" := nat_meet (at level 40, left associativity).
Local Infix "⇡" := nat_join (at level 50, left associativity).

Hint Resolve power2_gt_0.

Section stability_of_power.

  Fact mult_lt_power_2 u v k : u < power k 2 -> v < power k 2 -> u*v < power (2*k) 2.
  Proof.
(* Goal: forall (_ : lt (add l (S O)) q) (_ : forall (i : nat) (_ : lt i l), lt (f i) (@mscal nat mul (S O) q (S (S O)))), @sig nat (fun c : nat => is_cipher_of f c) *)
    intros H1 H2.
(* Goal: lt (mul u v) (@mscal nat mul (S O) (mul (S (S O)) k) (S (S O))) *)
    replace (2*k) with (k+k) by omega.
(* Goal: lt (mul u v) (@mscal nat mul (S O) (add k k) (S (S O))) *)
    rewrite power_plus.
(* Goal: lt (mul u v) (mul (@mscal nat mul (S O) k (S (S O))) (@mscal nat mul (S O) k (S (S O)))) *)
    apply lt_le_trans with ((S u)*S v).
(* Goal: lt (mul u v) (mul (S u) (S v)) *)
(* Goal: le (mul (S u) (S v)) (mul (@mscal nat mul (S O) k (S (S O))) (@mscal nat mul (S O) k (S (S O)))) *)
    simpl; rewrite (mult_comm _ (S _)); simpl; rewrite mult_comm; omega.
(* Goal: le (mul (S (S O)) (S (@mscal nat mul (S O) (S l) (S (S O))))) (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) *)
    apply mult_le_compat; auto.
  Qed.

  Fact mult_lt_power_2_4 u v k : u < power k 2 -> v < power k 2 -> u*v < power (4*k) 2.
  Proof.
(* Goal: forall (_ : lt (add l (S O)) q) (_ : forall (i : nat) (_ : lt i l), lt (f i) (@mscal nat mul (S O) q (S (S O)))), @sig nat (fun c : nat => is_cipher_of f c) *)
    intros H1 H2.
(* Goal: lt (mul u v) (@mscal nat mul (S O) (mul (S (S (S (S O)))) k) (S (S O))) *)
    apply lt_le_trans with (1 := mult_lt_power_2 _ H1 H2).
(* Goal: le (@mscal nat mul (S O) (S q) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) *)
    apply power_mono_l; omega.
  Qed.

  Fact mult_lt_power_2_4' u1 v1 u2 v2 k : 
               u1 < power k 2 
            -> v1 < power k 2
            -> u2 < power k 2
            -> v2 < power k 2
            -> u1*v1+v2*u2 < power (4*k) 2.
  Proof.
(* Goal: forall (_ : lt u1 (@mscal nat mul (S O) k (S (S O)))) (_ : lt v1 (@mscal nat mul (S O) k (S (S O)))) (_ : lt u2 (@mscal nat mul (S O) k (S (S O)))) (_ : lt v2 (@mscal nat mul (S O) k (S (S O)))), lt (add (mul u1 v1) (mul v2 u2)) (@mscal nat mul (S O) (mul (S (S (S (S O)))) k) (S (S O))) *)
    intros H1 H2 H3 H4.
(* Goal: lt (add (mul u1 v1) (mul v2 u2)) (@mscal nat mul (S O) (mul (S (S (S (S O)))) k) (S (S O))) *)
    destruct (eq_nat_dec k 0) as [ ? | Hk ].
    - subst k; simpl.
(* Goal: lt (add (mul u1 v1) (mul v2 u2)) (@mscal nat mul (S O) O (S (S O))) *)
      rewrite power_0 in *.
(* Goal: lt (add (mul u1 v1) (mul v2 u2)) (S O) *)
      destruct u1; destruct v1; destruct u2; destruct v2; subst; omega.
    - apply lt_le_trans with (power (S (2*k)) 2). 
      + rewrite power_S, <- mult_2_eq_plus.
(* Goal: lt (add (mul u1 v1) (mul v2 u2)) (add (@mscal nat mul (S O) (mul (S (S O)) k) (S (S O))) (@mscal nat mul (S O) (mul (S (S O)) k) (S (S O)))) *)
        apply plus_lt_compat; apply mult_lt_power_2; auto.
(* Goal: le (@mscal nat mul (S O) (S q) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) *)
      + apply power_mono_l; omega.
  Qed.

End stability_of_power.

Section power_decomp.

  Variable (p : nat) (Hp : 2 <= p).

  Let power_nzero x : power x p <> 0.
  Proof. generalize (@power_ge_1 x p); omega. Qed.

  Fact power_decomp_lt n f a q :  
           (forall i j, i < j < n -> f i < f j)
        -> (forall i, i < n -> f i < q)
        -> (forall i, i < n -> a i < p)
        -> ∑ n (fun i => a i * power (f i) p) < power q p.
  Proof.
(* Goal: forall (_ : forall (i j : nat) (_ : and (lt i j) (lt j n)), lt (f i) (f j)) (_ : forall (i : nat) (_ : lt i n), lt (f i) q) (_ : forall (i : nat) (_ : lt i n), lt (a i) p), lt (@msum nat add O n (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) (@mscal nat mul (S O) q p) *)
    revert q; induction n as [ | n IHn ]; intros q Hf1 Hf2 Ha.
    + rewrite msum_0; apply power_ge_1; omega.
    + rewrite msum_plus1; auto.
      apply lt_le_trans with (1*power (f n) p + a n * power (f n) p).
      * apply plus_lt_le_compat; auto.
(* Goal: lt (@msum nat add O n (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) (mul (S O) (@mscal nat mul (S O) (f n) p)) *)
        rewrite Nat.mul_1_l.
(* Goal: lt (@msum nat add O n (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) (@mscal nat mul (S O) (f n) p) *)
        apply IHn.
        - intros; apply Hf1; omega.
        - intros; apply Hf1; omega.
        - intros; apply Ha; omega.
      * rewrite <- Nat.mul_add_distr_r.
        replace q with (S (q-1)).
(* Goal: le (mul (S (S O)) (S (@mscal nat mul (S O) (S l) (S (S O))))) (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) *)
        - rewrite power_S; apply mult_le_compat; auto.
          ++ apply Ha; auto.
          ++ apply power_mono_l; try omega.
(* Goal: le (f n) (sub q (S O)) *)
             generalize (Hf2 n); intros; omega.
        - generalize (Hf2 0); intros; omega.
  Qed.

  Lemma power_decomp_is_digit n a f : 
           (forall i j, i < j < n -> f i < f j)
        -> (forall i, i < n -> a i < p)
        ->  forall i, i < n -> is_digit (∑ n (fun i => a i * power (f i) p)) p (f i) (a i).
  Proof.
(* Goal: forall (_ : forall (i j : nat) (_ : and (lt i j) (lt j n)), lt (f i) (f j)) (_ : forall (i : nat) (_ : lt i n), lt (a i) p) (i : nat) (_ : lt i n), is_digit (@msum nat add O n (fun i0 : nat => mul (a i0) (@mscal nat mul (S O) (f i0) p))) p (f i) (a i) *)
    intros Hf Ha.
(* Goal: forall (i : nat) (_ : lt i n), is_digit (@msum nat add O n (fun i0 : nat => mul (a i0) (@mscal nat mul (S O) (f i0) p))) p (f i) (a i) *)
    induction n as [ | n IHn ]; intros i Hi.
    + omega.
    + split; auto.
      exists (∑ (n-i) (fun j => a (S i + j) * power (f (S i+j) - f i - 1) p)), 
             (∑ i (fun j => a j * power (f j) p)); split.
      - replace (S n) with (S i + (n-i)) by omega.
(* Goal: @eq nat (@msum nat add O (add (S i) (sub n i)) (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) (add (mul (add (mul (@msum nat add O (sub n i) (fun j : nat => mul (a (add (S i) j)) (@mscal nat mul (S O) (sub (sub (f (add (S i) j)) (f i)) (S O)) p))) p) (a i)) (@mscal nat mul (S O) (f i) p)) (@msum nat add O i (fun j : nat => mul (a j) (@mscal nat mul (S O) (f j) p)))) *)
        rewrite msum_plus, msum_plus1; auto.
        rewrite <- plus_assoc, plus_comm; f_equal.
(* Goal: @eq nat (Nat.add (mul (a i) (@mscal nat mul (S O) (f i) p)) (@msum nat add O (sub n i) (fun i0 : nat => mul (a (add (S i) i0)) (@mscal nat mul (S O) (f (add (S i) i0)) p)))) (mul (add (mul (@msum nat add O (sub n i) (fun j : nat => mul (a (add (S i) j)) (@mscal nat mul (S O) (sub (sub (f (add (S i) j)) (f i)) (S O)) p))) p) (a i)) (@mscal nat mul (S O) (f i) p)) *)
        rewrite Nat.mul_add_distr_r, plus_comm; f_equal.
        rewrite <- mult_assoc, mult_comm, <- sum_0n_scal_l.
(* Goal: @eq nat (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (k i) r)) (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) r)) *)
        apply msum_ext.
(* Goal: forall (i0 : nat) (_ : lt i0 (sub n i)), @eq nat (mul (a (add (S i) i0)) (@mscal nat mul (S O) (f (add (S i) i0)) p)) (mul (Nat.mul p (@mscal nat mul (S O) (f i) p)) (mul (a (add (S i) i0)) (@mscal nat mul (S O) (sub (sub (f (add (S i) i0)) (f i)) (S O)) p))) *)
        intros j Hj.
        rewrite (mult_comm (_ * _));
        repeat rewrite <- mult_assoc; f_equal.
        rewrite <- power_S, <- power_plus; f_equal.
        generalize (Hf i (S i+j)); intros; omega.
      - apply power_decomp_lt; auto.
        * intros; apply Hf; omega.
        * intros; apply Ha; omega.
  Qed.

  Theorem power_decomp_unique n f a b :
            (forall i j, i < j < n -> f i < f j)
         -> (forall i, i < n -> a i < p)
         -> (forall i, i < n -> b i < p)
         -> ∑ n (fun i => a i * power (f i) p)
          = ∑ n (fun i => b i * power (f i) p)
         -> forall i, i < n -> a i = b i.
  Proof.
(* Goal: forall (_ : forall (i j : nat) (_ : and (lt i j) (lt j n)), lt (f i) (f j)) (_ : forall (i : nat) (_ : lt i n), lt (a i) p) (_ : forall (i : nat) (_ : lt i n), lt (b i) p) (_ : @eq nat (@msum nat add O n (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) (@msum nat add O n (fun i : nat => mul (b i) (@mscal nat mul (S O) (f i) p)))) (i : nat) (_ : lt i n), @eq nat (a i) (b i) *)
    intros Hf Ha Hb E i Hi.
    generalize (power_decomp_is_digit _ _ Hf Ha Hi)
               (power_decomp_is_digit _ _ Hf Hb Hi).
(* Goal: forall (_ : is_digit (@msum nat add O n (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) p (f i) (a i)) (_ : is_digit (@msum nat add O n (fun i : nat => mul (b i) (@mscal nat mul (S O) (f i) p))) p (f i) (b i)), @eq nat (a i) (b i) *)
    rewrite E; apply is_digit_fun.
  Qed.

End power_decomp.

Section power_decomp_uniq.

  Variable (p : nat) (Hp : 2 <= p).

  Theorem power_decomp_factor n f a : 
           (forall i, 0 < i < S n -> f 0 < f i)
        -> ∑ (S n) (fun i => a i * power (f i) p) 
         = ∑ n (fun i => a (S i) * power (f (S i) - f 0 - 1) p) * power (S (f 0)) p
         + a 0 * power (f 0) p.
  Proof.
(* Goal: forall _ : forall (i j : nat) (_ : and (lt i j) (lt j n)), lt (f i) (f j), @sig nat (fun q : nat => and (le q n) (and (forall (i : nat) (_ : lt i q), le (f i) h) (forall (i : nat) (_ : and (le q i) (lt i n)), lt h (f i)))) *)
    intros Hf.
(* Goal: @eq nat (@msum nat add O (S n) (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) (add (mul (@msum nat add O n (fun i : nat => mul (a (S i)) (@mscal nat mul (S O) (sub (sub (f (S i)) (f O)) (S O)) p))) (@mscal nat mul (S O) (S (f O)) p)) (mul (a O) (@mscal nat mul (S O) (f O) p))) *)
    rewrite msum_S, plus_comm; f_equal.
    rewrite <- sum_0n_scal_r.
(* Goal: @eq nat (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (k i) r)) (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) r)) *)
    apply msum_ext.
(* Goal: forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
    intros i Hi.
    rewrite <- mult_assoc; f_equal.
    rewrite <- power_plus; f_equal.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
    generalize (Hf (S i)); intros; omega.
  Qed.

  Let power_nzero x : power x p <> 0.
  Proof.
(* Goal: not (@eq nat (@mscal nat mul (S O) x p) O) *)
    generalize (@power_ge_1 x p); omega.
  Qed.

  Let lt_minus_cancel a b c : a < b < c -> b - a - 1 < c - a - 1.
  Proof. intros; omega. Qed. 

  (* Another proof of the above statement *)

  Theorem power_decomp_unique' n f a b :
            (forall i j, i < j < n -> f i < f j)
         -> (forall i, i < n -> a i < p)
         -> (forall i, i < n -> b i < p)
         -> ∑ n (fun i => a i * power (f i) p)
          = ∑ n (fun i => b i * power (f i) p)
         -> forall i, i < n -> a i = b i.
  Proof.
(* Goal: forall (_ : forall (i j : nat) (_ : and (lt i j) (lt j n)), lt (f i) (f j)) (_ : forall (i : nat) (_ : lt i n), lt (a i) p) (_ : forall (i : nat) (_ : lt i n), lt (b i) p) (_ : @eq nat (@msum nat add O n (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) (@msum nat add O n (fun i : nat => mul (b i) (@mscal nat mul (S O) (f i) p)))) (i : nat) (_ : lt i n), @eq nat (a i) (b i) *)
    revert f a b.
(* Goal: forall (f a b : forall _ : nat, nat) (_ : forall (i j : nat) (_ : and (lt i j) (lt j n)), lt (f i) (f j)) (_ : forall (i : nat) (_ : lt i n), lt (a i) p) (_ : forall (i : nat) (_ : lt i n), lt (b i) p) (_ : @eq nat (@msum nat add O n (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) (@msum nat add O n (fun i : nat => mul (b i) (@mscal nat mul (S O) (f i) p)))) (i : nat) (_ : lt i n), @eq nat (a i) (b i) *)
    induction n as [ | n IHn ]; intros f a b Hf Ha Hb.
    + intros; omega.
    + assert (forall i, 0 < i < S n -> f 0 < f i)
        by (intros; apply Hf; omega). 
(* Goal: forall (_ : @eq nat (@msum nat add O (S n) (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) (@msum nat add O (S n) (fun i : nat => mul (b i) (@mscal nat mul (S O) (f i) p)))) (i : nat) (_ : lt i (S n)), @eq nat (a i) (b i) *)
      do 2 (rewrite power_decomp_factor; auto).
(* Goal: forall (_ : @eq nat (@msum nat add O l (fun i : nat => mul (mul (a i) (S O)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat add O l (fun i : nat => mul (mul (b i) (c i)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
      intros E.
(* Goal: forall (i : nat) (_ : lt i (S n)), @eq nat (a i) (b i) *)
      apply div_rem_uniq in E; auto.
      * destruct E as (E1 & E2).
(* Goal: forall (i : nat) (_ : lt i (S n)), @eq nat (a i) (b i) *)
        intros [ | i ] Hi.
        - revert E2; rewrite Nat.mul_cancel_r; auto.
        - apply IHn with (4 := E1); try omega.
          ++ intros u j Hu; apply lt_minus_cancel; split; apply Hf; omega. 
          ++ intros; apply Ha; omega.
          ++ intros; apply Hb; omega.
      * rewrite power_S.
(* Goal: lt (mul (b O) (@mscal nat mul (S O) (f O) p)) (mul p (@mscal nat mul (S O) (f O) p)) *)
        apply Nat.mul_lt_mono_pos_r.
        - apply power_ge_1; omega.
        - apply Ha; omega.
      * rewrite power_S.
(* Goal: lt (mul (b O) (@mscal nat mul (S O) (f O) p)) (mul p (@mscal nat mul (S O) (f O) p)) *)
        apply Nat.mul_lt_mono_pos_r.
        - apply power_ge_1; omega.
        - apply Hb; omega.
  Qed.

End power_decomp_uniq.

Fact mult_2_eq_plus x : x + x = 2 *x.
Proof. ring. Qed.

Section power_injective.

  Let power_2_inj_1 i j n : j < i -> 2* power n 2 <> power i 2 + power j 2.
  Proof.
    rewrite <- power_S; intros H4 E.
(* Goal: False *)
     generalize (@power_ge_1 j 2); intro C.
(* Goal: False *)
     destruct (lt_eq_lt_dec i (S n)) as [ [ H5 | H5 ] | H5 ].
     + apply power_mono_l with (x := 2) in H5; auto.
(* Goal: False *)
       rewrite power_S in H5.
(* Goal: False *)
       apply power_mono_l with (x := 2) in H4; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
       rewrite power_S in H4; omega.
     + subst i; omega.
     + apply power_mono_l with (x := 2) in H5; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      rewrite power_S in H5; omega.
  Qed.

  Fact power_2_n_ij_neq i j n : i <> j -> power (S n) 2 <> power i 2 + power j 2.
  Proof.
(* Goal: forall _ : @eq nat (add (S O) (mul (sub r (S O)) w)) (@mscal nat mul (S O) l r), @eq nat w (@msum nat add O l (fun i : nat => @mscal nat mul (S O) i r)) *)
    intros H.
(* Goal: not (@eq nat (@mscal nat mul (S O) (S n) (S (S O))) (add (@mscal nat mul (S O) i (S (S O))) (@mscal nat mul (S O) j (S (S O))))) *)
    destruct (lt_eq_lt_dec i j) as [ [] | ]; try tauto.
    + rewrite plus_comm; apply power_2_inj_1; auto.
    + apply power_2_inj_1; auto.
  Qed.

  Fact power_2_inj i j : power i 2 = power j 2 -> i = j.
  Proof.
(* Goal: forall _ : @eq nat (add (S O) (mul (sub r (S O)) w)) (@mscal nat mul (S O) l r), @eq nat w (@msum nat add O l (fun i : nat => @mscal nat mul (S O) i r)) *)
    intros H.
    destruct (lt_eq_lt_dec i j) as [ [ C | C ] | C ]; auto;
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      apply power_smono_l with (x := 2) in C; omega.
  Qed.

  Let power_plus_lt a b c : a < b < c -> power a 2 + power b 2 < power c 2.
  Proof.
(* Goal: forall _ : and (lt a b) (lt b c), lt (add (@mscal nat mul (S O) a (S (S O))) (@mscal nat mul (S O) b (S (S O)))) (@mscal nat mul (S O) c (S (S O))) *)
    intros [ H1 H2 ].
(* Goal: lt (add (@mscal nat mul (S O) a (S (S O))) (@mscal nat mul (S O) b (S (S O)))) (@mscal nat mul (S O) c (S (S O))) *)
    apply power_mono_l with (x := 2) in H2; auto.
(* Goal: lt (add (@mscal nat mul (S O) a (S (S O))) (@mscal nat mul (S O) b (S (S O)))) (@mscal nat mul (S O) c (S (S O))) *)
    apply power_smono_l with (x := 2) in H1; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
    rewrite power_S in H2; omega.
  Qed.

  Let power_inj_2 i1 j1 i2 j2 : 
             j1 < i1 
          -> j2 < i2 
          -> power i1 2 + power j1 2 = power i2 2 + power j2 2
          -> i1 = i2 /\ j1 = j2.
  Proof.
(* Goal: forall (_ : le (S O) x) (_ : @eq nat (add (S O) (mul x a)) y) (_ : @eq nat (add (S O) (mul x b)) y), @eq nat a b *)
    intros H1 H2 H3.
(* Goal: and (@eq nat i1 i2) (@eq nat j1 j2) *)
    destruct (lt_eq_lt_dec i1 i2) as [ [ C | C ] | C ].
    + generalize (@power_plus_lt j1 i1 i2); intros; omega.
    + split; auto; apply power_2_inj; subst; omega.
    + generalize (@power_plus_lt j2 i2 i1); intros; omega.
  Qed.

  Theorem sum_2_power_2_injective i1 j1 i2 j2 :
              j1 <= i1 
           -> j2 <= i2 
           -> power i1 2 + power j1 2 = power i2 2 + power j2 2 
           -> i1 = i2 /\ j1 = j2.
  Proof.
(* Goal: forall (_ : le j1 i1) (_ : le j2 i2) (_ : @eq nat (add (@mscal nat mul (S O) i1 (S (S O))) (@mscal nat mul (S O) j1 (S (S O)))) (add (@mscal nat mul (S O) i2 (S (S O))) (@mscal nat mul (S O) j2 (S (S O))))), and (@eq nat i1 i2) (@eq nat j1 j2) *)
    intros H1 H2 E.
    destruct (eq_nat_dec i1 j1) as [ H3 | H3 ];
    destruct (eq_nat_dec i2 j2) as [ H4 | H4 ].
    + subst j1 j2.
(* Goal: and (@eq nat i1 i2) (@eq nat i1 i2) *)
      assert (i1 = i2); auto.
      do 2 rewrite mult_2_eq_plus, <- power_S in E.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      apply power_2_inj in E; omega.
    + subst j1; rewrite mult_2_eq_plus in E.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      apply power_2_inj_1 in E; omega.
    + subst j2; symmetry in E.
(* Goal: and (@eq nat i1 i2) (@eq nat j1 i2) *)
      rewrite mult_2_eq_plus in E.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      apply power_2_inj_1 in E; omega.
    + revert E; apply power_inj_2; omega.
  Qed. 
 
End power_injective.

Fact divides_power p a b : a <= b -> divides (power a p) (power b p).
Proof.
  (* split. *)
  * induction 1 as [ | b H IH ].
    + apply divides_refl.
    + apply divides_trans with (1 := IH).
(* Goal: divides (@mscal nat mul (S O) b p) (@mscal nat mul (S O) (S b) p) *)
      rewrite power_S; apply divides_mult, divides_refl.
(*  * intros H.
    apply divides_le in H. *)
Qed.

Fact divides_msum k n f : (forall i, i < n -> divides k (f i)) -> divides k (∑ n f).
Proof.
(* Goal: forall _ : forall (i j : nat) (_ : and (lt i j) (lt j n)), lt (f i) (f j), @sig nat (fun p : nat => and (le p n) (and (forall (i : nat) (_ : lt i p), lt (f i) k) (forall (i : nat) (_ : and (le p i) (lt i n)), le k (f i)))) *)
  revert f; induction n as [ | n IHn ]; intros f Hf.
  + rewrite msum_0; apply divides_0.
  + rewrite msum_S; apply divides_plus.
    * apply Hf; omega.
    * apply IHn; intros; apply Hf; omega.
Qed.

Fact inc_seq_split_lt n f k : 
         (forall i j, i < j < n -> f i < f j) 
      -> { p | p <= n /\ (forall i, i < p -> f i < k) /\ forall i, p <= i < n -> k <= f i }.
Proof.
(* Goal: forall _ : forall (i j : nat) (_ : and (lt i j) (lt j n)), lt (f i) (f j), @sig nat (fun p : nat => and (le p n) (and (forall (i : nat) (_ : lt i p), lt (f i) k) (forall (i : nat) (_ : and (le p i) (lt i n)), le k (f i)))) *)
  revert f; induction n as [ | n IHn ]; intros f Hf.
  + exists 0; split; auto; split; intros; omega.
  + destruct (le_lt_dec k (f 0)) as [ H | H ].
    - exists 0; split; try omega.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      split; intros i Hi; try omega.
(* Goal: le k (f i) *)
      destruct i as [ | i ]; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      apply le_trans with (1 := H), lt_le_weak, Hf; omega.
    - destruct (IHn (fun i => f (S i))) as (p & H1 & H2 & H3).
      * intros; apply Hf; omega.
      * exists (S p); split; try omega; split.
        ++ intros [ | i ] Hi; auto; apply H2; omega.
        ++ intros [ | i ] Hi; try omega; apply H3; omega.
Qed.

Fact inc_seq_split_le n f h : (forall i j, i < j < n -> f i < f j) 
                   -> { q | q <= n 
                         /\ (forall i, i < q      -> f i <= h)
                         /\ (forall i, q <= i < n -> h < f i) }.
Proof.
(* Goal: forall _ : forall (i j : nat) (_ : and (lt i j) (lt j n)), lt (f i) (f j), @sig nat (fun q : nat => and (le q n) (and (forall (i : nat) (_ : lt i q), le (f i) h) (forall (i : nat) (_ : and (le q i) (lt i n)), lt h (f i)))) *)
  intros Hf.
  destruct inc_seq_split_lt with (1 := Hf) (k := S h)
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
    as (q & H1 & H2 & H3); exists q; split; auto; split.
  + intros i Hi; specialize (H2 _ Hi); omega.
  + intros i Hi; specialize (H3 _ Hi); omega.
Qed.

Fact divides_lt p q : q < p -> divides p q -> q = 0.
Proof.
(* Goal: forall (_ : lt q p) (_ : divides p q), @eq nat q O *)
  intros H1 ([ | k] & H2); auto.
  revert H2; simpl; generalize (k *p); intros; omega.
Qed.

Fact sum_powers_inc_lt_last n f r : 
        2 <= r
     -> (forall i j, i < j <= n -> f i < f j)
     -> ∑ (S n) (fun i => power (f i) r) < power (S (f n)) r.
Proof.
(* Goal: forall (_ : le (S (S O)) r) (_ : forall (i j : nat) (_ : and (lt i j) (le j n)), lt (f i) (f j)), lt (@msum nat add O (S n) (fun i : nat => @mscal nat mul (S O) (f i) r)) (@mscal nat mul (S O) (S (f n)) r) *)
  intros Hr.
(* Goal: forall _ : forall (i j : nat) (_ : and (lt i j) (le j n)), lt (f i) (f j), lt (@msum nat add O (S n) (fun i : nat => @mscal nat mul (S O) (f i) r)) (@mscal nat mul (S O) (S (f n)) r) *)
  revert f.
(* Goal: forall (f : forall _ : nat, nat) (_ : forall (i j : nat) (_ : and (lt i j) (le j n)), lt (f i) (f j)), lt (@msum nat add O (S n) (fun i : nat => @mscal nat mul (S O) (f i) r)) (@mscal nat mul (S O) (S (f n)) r) *)
  induction n as [ | n IHn ]; intros f Hf.
  + rewrite msum_1; auto; apply power_smono_l; auto.
  + rewrite msum_plus1; auto.
(* Goal: le (S (S O)) (@mscal nat mul (S O) (S l) (S (S O))) *)
    rewrite power_S.
    apply lt_le_trans with (power (S (f n)) r + power (f (S n)) r).
    * apply plus_lt_compat_r; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      apply IHn; intros; apply Hf; omega.
    * assert (power (S (f n)) r <= power (f (S n)) r) as H.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      { apply power_mono_l; try omega; apply Hf; omega. }
      apply le_trans with (2 * power (f (S n)) r); try omega.
(* Goal: le (mul (S (S O)) (S (@mscal nat mul (S O) (S l) (S (S O))))) (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) *)
      apply mult_le_compat; auto.
Qed.

Fact sum_powers_inc_lt n f p r : 
        2 <= r
     -> (forall i, i < n -> f i < p)
     -> (forall i j, i < j < n -> f i < f j)
     -> ∑ n (fun i => power (f i) r) < power p r.
Proof.
(* Goal: forall (_ : le (S (S O)) r) (_ : forall (i : nat) (_ : lt i n), lt (f i) p) (_ : forall (i j : nat) (_ : and (lt i j) (lt j n)), lt (f i) (f j)), lt (@msum nat add O n (fun i : nat => @mscal nat mul (S O) (f i) r)) (@mscal nat mul (S O) p r) *)
  destruct n as [ | n ].
  + intros H _ _; rewrite msum_0; apply power_ge_1; omega.
  + intros H1 H2 H3.
(* Goal: lt (@msum nat add O (S n) (fun i : nat => @mscal nat mul (S O) (f i) r)) (@mscal nat mul (S O) p r) *)
    apply lt_le_trans with (power (S (f n)) r).
    * apply sum_powers_inc_lt_last; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      intros; apply H3; omega.
    * apply power_mono_l; try omega.
(* Goal: le (S (f n)) p *)
      apply H2; auto.
Qed.

(* the value r^f1 + ... + f^fn uniquely determines n and f1 < ... < fn  *)

Fact sum_powers_injective r n f m g :
       2 <= r
    -> (forall i j, i < j < n -> f i < f j)
    -> (forall i j, i < j < m -> g i < g j)
    -> ∑ n (fun i => power (f i) r) = ∑ m (fun i => power (g i) r)
    -> n = m /\ forall i, i < n -> f i = g i.
Proof.
(* Goal: forall (_ : le (S (S O)) r) (_ : forall (i j : nat) (_ : and (lt i j) (lt j n)), lt (f i) (f j)) (_ : forall (i j : nat) (_ : and (lt i j) (lt j m)), lt (g i) (g j)) (_ : @eq nat (@msum nat add O n (fun i : nat => @mscal nat mul (S O) (f i) r)) (@msum nat add O m (fun i : nat => @mscal nat mul (S O) (g i) r))), and (@eq nat n m) (forall (i : nat) (_ : lt i n), @eq nat (f i) (g i)) *)
  intros Hr; revert m f g.
(* Goal: forall (m : nat) (f g : forall _ : nat, nat) (_ : forall (i j : nat) (_ : and (lt i j) (lt j n)), lt (f i) (f j)) (_ : forall (i j : nat) (_ : and (lt i j) (lt j m)), lt (g i) (g j)) (_ : @eq nat (@msum nat add O n (fun i : nat => @mscal nat mul (S O) (f i) r)) (@msum nat add O m (fun i : nat => @mscal nat mul (S O) (g i) r))), and (@eq nat n m) (forall (i : nat) (_ : lt i n), @eq nat (f i) (g i)) *)
  induction n as [ | n IHn ]; intros m f g Hf Hg.
  + rewrite msum_0.
(* Goal: forall _ : @eq nat (@msum nat add O (S n) (fun i : nat => @mscal nat mul (S O) (f i) r)) (@msum nat add O m (fun i : nat => @mscal nat mul (S O) (g i) r)), and (@eq nat (S n) m) (forall (i : nat) (_ : lt i (S n)), @eq nat (f i) (g i)) *)
    destruct m as [ | m ].
    * rewrite msum_0; split; auto; intros; omega.
    * rewrite msum_S.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      generalize (@power_ge_1 (g 0) r); intros; exfalso; omega.
  + destruct m as [ | m ].
    * rewrite msum_0, msum_S; intros; exfalso.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
       generalize (@power_ge_1 (f 0) r); intros; exfalso; omega.
    * destruct (lt_eq_lt_dec (f n) (g m)) as [ [E|E]| E].
      - rewrite msum_plus1 with (n := m); auto. 
(* Goal: forall _ : @eq nat (add (@msum nat add O n (fun i : nat => @mscal nat mul (S O) (f i) r)) (@mscal nat mul (S O) (f n) r)) (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (g i) r)), and (@eq nat (S n) (S m)) (forall (i : nat) (_ : lt i (S n)), @eq nat (f i) (g i)) *)
        intros; exfalso.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        assert (∑ (S n) (fun i => power (f i) r) < power (g m) r) as C; try omega.
(* Goal: lt (@msum nat add O (S (S m)) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S l) (S (S O))) r) *)
        apply sum_powers_inc_lt; auto.
(* Goal: forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
        intros i Hi.
(* Goal: lt (f i) (g m) *)
        destruct (eq_nat_dec i n); subst; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        apply lt_trans with (2 := E), Hf; omega.
      - do 2 (rewrite msum_plus1; auto); intros C.
(* Goal: and (@eq nat (S n) (S m)) (forall (i : nat) (_ : lt i (S n)), @eq nat (f i) (g i)) *)
        destruct (IHn m f g) as (H1 & H2).
        ++ intros; apply Hf; omega.
        ++ intros; apply Hg; omega.
        ++ rewrite E in C; omega.
        ++ split; subst; auto.
(* Goal: forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
           intros i Hi.
(* Goal: le (k i) (k m) *)
           destruct (eq_nat_dec i m); subst; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
           apply H2; omega.
      - rewrite msum_plus1 with (n := n); auto. 
(* Goal: forall _ : @eq nat (add (@msum nat add O n (fun i : nat => @mscal nat mul (S O) (f i) r)) (@mscal nat mul (S O) (f n) r)) (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (g i) r)), and (@eq nat (S n) (S m)) (forall (i : nat) (_ : lt i (S n)), @eq nat (f i) (g i)) *)
        intros; exfalso.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        assert (∑ (S m) (fun i => power (g i) r) < power (f n) r) as C; try omega.
(* Goal: lt (@msum nat add O (S (S m)) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S l) (S (S O))) r) *)
        apply sum_powers_inc_lt; auto.
(* Goal: forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
        intros i Hi.
(* Goal: le (k i) (k m) *)
        destruct (eq_nat_dec i m); subst; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        apply lt_trans with (2 := E), Hg; omega.
Qed.

Fact power_divides_sum_power r p n f :
         2 <= r 
      -> 0 < n
      -> (forall i j, i < j < n -> f i < f j) 
      -> divides (power p r) (∑ n (fun i => power (f i) r)) <-> p <= f 0.
Proof.
  intros Hr Hn Hf.
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
  split.
  + destruct inc_seq_split_lt with (k := p) (1 := Hf) as (k & H1 & H2 & H3).
    replace n with (k+(n-k)) by omega.
    rewrite msum_plus; auto.
(* Goal: forall _ : @eq nat (add (S O) (mul (sub r (S O)) w)) (@mscal nat mul (S O) l r), @eq nat w (@msum nat add O l (fun i : nat => @mscal nat mul (S O) i r)) *)
    rewrite plus_comm; intros H.
    apply divides_plus_inv in H.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
    2: apply divides_msum; intros; apply divides_power, H3; omega.
    destruct k as [ | k ].
    * apply H3; omega.
    * apply divides_lt in H.
      - rewrite msum_S in H.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        generalize (@power_ge_1 (f 0) r); intros; omega.
      - apply sum_powers_inc_lt; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        intros; apply Hf; omega.
  + intros H.
(* Goal: divides (@mscal nat mul (S O) (S (S (S (S O)))) r) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) r)) *)
    apply divides_msum.
    intros i Hi; apply divides_power.
    apply le_trans with (1 := H).
    destruct i; auto. 
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
    generalize (Hf 0 (S i)); intros; omega.
Qed.

Fact smono_upto_injective n f :
       (forall i j, i < j < n -> f i < f j)
    -> (forall i j, i < n -> j < n -> f i = f j -> i = j).
Proof.
(* Goal: forall (_ : forall (i j : nat) (_ : and (lt i j) (lt j n)), lt (f i) (f j)) (i j : nat) (_ : lt i n) (_ : lt j n) (_ : @eq nat (f i) (f j)), @eq nat i j *)
  intros Hf i j Hi Hj E.
(* Goal: @eq nat i j *)
  destruct (lt_eq_lt_dec i j) as [ [H|] | H ]; auto.
  + generalize (@Hf i j); intros; omega.
  + generalize (@Hf j i); intros; omega.
Qed.

Fact product_sums n f g : (∑ n f)*(∑ n g) 
                         = ∑ n (fun i => f i*g i) 
                         + ∑ n (fun i => ∑ i (fun j => f i*g j + f j*g i)).
Proof.
(* Goal: @eq nat (mul (@msum nat add O n f) (@msum nat add O n g)) (add (@msum nat add O n (fun i : nat => mul (f i) (g i))) (@msum nat add O n (fun i : nat => @msum nat add O i (fun j : nat => add (mul (f i) (g j)) (mul (f j) (g i)))))) *)
  induction n as [ | n IHn ].
  + repeat rewrite msum_0; auto.
  + repeat rewrite msum_plus1; auto.
(* Goal: @eq nat (mul (add (@msum nat add O n f) (f n)) (add (@msum nat add O n g) (g n))) (add (add (@msum nat add O n (fun i : nat => mul (f i) (g i))) (mul (f n) (g n))) (add (@msum nat add O n (fun i : nat => @msum nat add O i (fun j : nat => add (mul (f i) (g j)) (mul (f j) (g i))))) (@msum nat add O n (fun j : nat => add (mul (f n) (g j)) (mul (f j) (g n)))))) *)
    repeat rewrite Nat.mul_add_distr_l.
(* Goal: @eq nat (Nat.add (Nat.mul (add (@msum nat add O n f) (f n)) (@msum nat add O n g)) (Nat.mul (add (@msum nat add O n f) (f n)) (g n))) (add (add (@msum nat add O n (fun i : nat => mul (f i) (g i))) (mul (f n) (g n))) (add (@msum nat add O n (fun i : nat => @msum nat add O i (fun j : nat => add (mul (f i) (g j)) (mul (f j) (g i))))) (@msum nat add O n (fun j : nat => add (mul (f n) (g j)) (mul (f j) (g n)))))) *)
    repeat rewrite Nat.mul_add_distr_r.
(* Goal: @eq nat (Nat.add (Nat.add (Nat.mul (@msum nat add O n f) (@msum nat add O n g)) (Nat.mul (f n) (@msum nat add O n g))) (Nat.add (Nat.mul (@msum nat add O n f) (g n)) (Nat.mul (f n) (g n)))) (add (add (@msum nat add O n (fun i : nat => mul (f i) (g i))) (mul (f n) (g n))) (add (@msum nat add O n (fun i : nat => @msum nat add O i (fun j : nat => add (mul (f i) (g j)) (mul (f j) (g i))))) (@msum nat add O n (fun j : nat => add (mul (f n) (g j)) (mul (f j) (g n)))))) *)
    rewrite IHn, msum_sum; auto.
    * rewrite sum_0n_scal_l, sum_0n_scal_r; ring.
    * intros; ring.
Qed.

Section sums.

  Fact square_sum n f : (∑ n f)*(∑ n f) = ∑ n (fun i => f i*f i) + 2*∑ n (fun i => ∑ i (fun j => f i*f j)).
  Proof.
    rewrite product_sums, <- sum_0n_scal_l; f_equal.
    apply msum_ext; intros; rewrite <- sum_0n_scal_l.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
    apply msum_ext; intros; ring.
  Qed. 

  Fact sum_regroup r k n f :
          (forall i, i < n -> f i < k) 
       -> (forall i j, i < j < n -> f i < f j)
       -> { g | ∑ n (fun i => power (f i) r) 
              = ∑ k (fun i => g i * power i r) 
             /\ (forall i, i < k  -> g i <= 1) 
             /\ (forall i, k <= i -> g i = 0) }.
  Proof.
    revert k f; induction n as [ | n IHn ]; intros k f Hf1 Hf2.
    + exists (fun _ => 0); split; auto.
      rewrite msum_0, msum_of_unit; auto.
    + destruct (IHn (f n) f) as (g & H1 & H2 & H3).
      * intros; apply Hf2; omega.
      * intros; apply Hf2; omega.
      * exists (fun i => if eq_nat_dec i (f n) then 1 else g i).
        split; [ | split ].
        - rewrite msum_plus1, H1; auto.
          replace k with (f n + S (k - f n -1)).
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          2: generalize (Hf1 n); intros; omega.
          rewrite msum_plus; auto; f_equal.
          ++ apply msum_ext.
             intros i He.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
             destruct (eq_nat_dec i (f n)); try ring; omega.
          ++ rewrite msum_S, msum_of_unit; auto.
             ** repeat (rewrite plus_comm; simpl). 
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
                destruct (eq_nat_dec (f n) (f n)); try ring; omega.
             ** intros i Hi.
                destruct (eq_nat_dec (f n+S i) (f n)); try omega.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
                rewrite H3; omega.
        - intros i Hi.
          destruct (eq_nat_dec i (f n)); auto.
          destruct (le_lt_dec (f n) i).
          ++ rewrite H3; omega.
          ++ apply H2; omega.
        - intros i Hi.
          generalize (Hf1 n); intros.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          destruct (eq_nat_dec i (f n)); try omega.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          apply H3; omega.
  Qed.
 
  Section sum_sum_regroup.

    Variable (r n k : nat) (f : nat -> nat)
             (Hf1 : forall i, i < n -> f i <= k) 
             (Hf2 : forall i j, i < j < n -> f i < f j).

    Theorem sum_sum_regroup : { g | ∑ n (fun i => ∑ i (fun j => power (f i + f j) r))
                                  = ∑ (2*k) (fun i => g i * power i r) 
                                  /\ forall i, g i <= n }.
    Proof.
      revert n f Hf1 Hf2. 
      induction n as [ | p IHp ]; intros f Hf1 Hf2.
      + exists (fun _ => 0); split; auto.
(* Goal: forall _ : @eq nat (@msum nat add O O (fun i : nat => @mscal nat mul (S O) (f i) r)) (@msum nat add O m (fun i : nat => @mscal nat mul (S O) (g i) r)), and (@eq nat O m) (forall (i : nat) (_ : lt i O), @eq nat (f i) (g i)) *)
        rewrite msum_0.
        simpl; rewrite msum_of_unit; auto.
      + destruct (IHp f) as (g & H1 & H2).
        * intros; apply Hf1; omega.
        * intros; apply Hf2; omega.
        * destruct sum_regroup with (r := r) (n := p) (f := fun j => f p + f j) (k := 2*k)
            as (g1 & G1 & G2 & G3).
          - intros i Hi; generalize (@Hf1 p) (@Hf2 i p); intros; omega.
          - intros i j H; generalize (@Hf2 i j); intros; omega.
          - assert (forall i, g1 i <= 1) as G4.
            { intro i; destruct (le_lt_dec (2*k) i); auto; rewrite G3; omega. }
            exists (fun i => g i + g1 i); split.
            ++ rewrite msum_plus1; auto.
               rewrite H1, G1, <- msum_sum; auto.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
               2: intros; ring.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
               apply msum_ext; intros; ring.
            ++ intros i.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
               generalize (H2 i) (G4 i); intros; omega.
    Qed.

  End sum_sum_regroup.

  Section all_ones.

    Let equation_inj x y a b : 1 <= x -> 1+x*a = y -> 1+x*b = y -> a = b.
    Proof.
(* Goal: forall (_ : le (S O) x) (_ : @eq nat (add (S O) (mul x a)) y) (_ : @eq nat (add (S O) (mul x b)) y), @eq nat a b *)
      intros H1 H2 H3.
      rewrite <- H3 in H2; clear y H3.
      rewrite <- (@Nat.mul_cancel_l _ _ x); omega.
    Qed.

    Variables (r : nat) (Hr : 2 <= r).

    Fact all_ones_equation l : 1+(r-1)*∑ l (fun i => power i r) = power l r.
    Proof.
(* Goal: @eq nat (add (S O) (mul (sub r (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) i r)))) (@mscal nat mul (S O) l r) *)
      induction l as [ | l IHl ].
      * rewrite msum_0, Nat.mul_0_r, power_0; auto.
(* Goal: @eq nat (add (S O) (mul (sub r (S O)) (@msum nat add O (S l) (fun i : nat => @mscal nat mul (S O) i r)))) (@mscal nat mul (S O) (S l) r) *)
      * rewrite msum_plus1; auto.
(* Goal: @eq nat (add (S O) (mul (sub r (S O)) (add (@msum nat add O l (fun i : nat => @mscal nat mul (S O) i r)) (@mscal nat mul (S O) l r)))) (@mscal nat mul (S O) (S l) r) *)
        rewrite Nat.mul_add_distr_l, power_S.
        replace r with (1+(r-1)) at 4 by omega.
(* Goal: @eq nat (add (S O) (Nat.add (Nat.mul (sub r (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) i r))) (Nat.mul (sub r (S O)) (@mscal nat mul (S O) l r)))) (mul (add (S O) (sub r (S O))) (@mscal nat mul (S O) l r)) *)
        rewrite Nat.mul_add_distr_r.
        rewrite <- IHl at 2; ring.
    Qed.

    Fact all_ones_dio l w : w = ∑ l (fun i => power i r) <-> 1+(r-1)*w = power l r.
    Proof.
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      split.
      + intros; subst; apply all_ones_equation.
      + intros H.
(* Goal: @eq nat w (@msum nat add O l (fun i : nat => @mscal nat mul (S O) i r)) *)
        apply equation_inj with (2 := H).
        * omega.
        * apply all_ones_equation.
    Qed.

  End all_ones.

  Section const_1.

    Variable (l q : nat) (Hl : 0 < l) (Hlq : l+1 < q).

    Let Hq : 1 <= q.     Proof. omega. Qed. 
    Let Hq' : 0 < 4*q.   Proof. omega. Qed.
    
    Let r := (power (4*q) 2).

    Let Hr' : 4 <= r.    Proof. apply (@power_mono_l 2 (4*q) 2); omega. Qed.
    Let Hr :  2 <= r.    Proof. omega. Qed.

    Section all_ones.

      Variable (n w : nat) (Hw : w = ∑ n (fun i => power i r)).

      Let Hw_0 : w = ∑ n (fun i => 1*power i r).
      Proof. rewrite Hw; apply msum_ext; intros; ring. Qed.

      Fact all_ones_joins : w = msum nat_join 0 n (fun i => 1*power i r).
      Proof. 
(* Goal: @eq nat w (@msum nat nat_join O n (fun i : nat => mul (S O) (@mscal nat mul (S O) i r))) *)
        rewrite Hw_0.
        apply sum_powers_ortho with (q := 4*q); auto; try omega.
      Qed.

      Let Hw_1 : 2*w = ∑ n (fun i => 2*power i r).
      Proof. 
        rewrite Hw_0, <- sum_0n_scal_l.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
        apply msum_ext; intros; ring.
      Qed.

      Fact all_ones_2_joins : 2*w = msum nat_join 0 n (fun i => 2*power i r).
      Proof.
(* Goal: @eq nat (mul (S (S O)) w) (@msum nat nat_join O n (fun i : nat => mul (S (S O)) (@mscal nat mul (S O) i r))) *)
        rewrite Hw_1.
        apply sum_powers_ortho with (q := 4*q); auto; try omega.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        intros; omega.
      Qed.

    End all_ones.

    Section increase.
   
      Variable (m k k' u w : nat) (f : nat -> nat) 
               (Hm : 2*m < r) 
               (Hf1 : forall i, i < m -> f i <= k)
               (Hf2 : forall i j, i < j < m  -> f i < f j)
               (Hw : w = ∑ k' (fun i => power i r))
               (Hu : u = ∑ m (fun i => power (f i) r)).

      Let Hf4 : forall i j, i < m -> j < m -> f i = f j -> i = j.
      Proof. apply smono_upto_injective; auto. Qed.

      Let u1 := ∑ m (fun i => power (2*f i) r).
      Let u2 := ∑ m (fun i => ∑ i (fun j => 2*power (f i + f j) r)).

      Fact const_u_square : u * u = u1 + u2.
      Proof.
(* Goal: @eq nat (mul u u) (add u1 u2) *)
        unfold u1, u2.
(* Goal: @eq nat (mul u u) (add (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (mul (S (S O)) (f1 i)) r)) (@msum nat add O (S m) (fun i : nat => @msum nat add O i (fun j : nat => mul (S (S O)) (@mscal nat mul (S O) (add (f1 i) (f1 j)) r))))) *)
        rewrite Hu, square_sum; f_equal.
        + apply msum_ext; intros; rewrite <- power_plus; f_equal; omega.
        + rewrite <- sum_0n_scal_l; apply msum_ext; intros i Hi.
          rewrite <- sum_0n_scal_l; apply msum_ext; intros j Hj.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
          rewrite power_plus; ring.
      Qed.

      Let Hu1_0 : u1 = ∑ m (fun i => 1*power (2*f i) r).
      Proof. apply msum_ext; intros; ring. Qed.

      Let Hseq_u a : a <= m -> ∑ a (fun i => 1*power (2*f i) r) = msum nat_join 0 a (fun i => 1*power (2*f i) r).
      Proof.
(* Goal: forall _ : le a m, @eq nat (@msum nat add O a (fun i : nat => mul (S O) (@mscal nat mul (S O) (mul (S (S O)) (f i)) r))) (@msum nat nat_join O a (fun i : nat => mul (S O) (@mscal nat mul (S O) (mul (S (S O)) (f i)) r))) *)
        intros Ha.
        apply sum_powers_ortho with (q := 4*q); auto; try omega.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        intros i j Hi Hj ?; apply Hf4; omega.
      Qed.

      Let Hu1 : u1 = msum nat_join 0 m (fun i => 1*power (2*f i) r).
      Proof. 
(* Goal: @eq nat u1 (@msum nat nat_join O m (fun i : nat => mul (S O) (@mscal nat mul (S O) (mul (S (S O)) (f i)) r))) *)
        rewrite Hu1_0; apply Hseq_u; auto.
      Qed.

      Let Hu2_0 : u2 = 2 * ∑ m (fun i => ∑ i (fun j => power (f i + f j) r)).
      Proof.
        unfold u2; rewrite <- sum_0n_scal_l; apply msum_ext.
        intros; rewrite <- sum_0n_scal_l; apply msum_ext; auto.
      Qed.

      (* MAJOR change in the argumentation ... one cannot show
         in generalize that the powers r^(f i + f j) are distincts
         powers for the values j < i < n, hence it is not correct
         than the sum reduces to a join ... it works when 
         f i = 2^i but not for an arbitrary (increasing function) f 

         So we rewrite ∑ {j < i < n} r^(f i + f j) as
            ∑ {i < k} (g i)*r^i for some small g i <= n
         supposing n is low compared to r *) 
         

      Let g_full : { g | ∑ m (fun i => ∑ i (fun j => power (f i + f j) r))
                      = ∑ (2*k) (fun i : nat => g i * power i r) 
                      /\ forall i : nat, g i <= m }.
      Proof. apply sum_sum_regroup; auto. Qed.
 
      Let g := proj1_sig g_full.
      Let Hg1 : u2 = ∑ (2*k) (fun i => (2*g i) * power i r).
      Proof. 
        rewrite Hu2_0, (proj1 (proj2_sig g_full)), <- sum_0n_scal_l.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
        apply msum_ext; unfold g; intros; ring.
      Qed.

      Let Hg2 i : 2*g i <= 2*m.
      Proof. apply mult_le_compat; auto; apply (proj2_sig g_full). Qed.

      Let Hg3 i : 2*g i < r.
      Proof. apply le_lt_trans with (1 := Hg2 _); auto. Qed.

      Let Hu2 : u2 = msum nat_join 0 (2*k) (fun i => (2*g i) * power i r).  
      Proof.
(* Goal: @eq nat u2 (@msum nat nat_join O (mul (S (S O)) k) (fun i : nat => mul (mul (S (S O)) (g i)) (@mscal nat mul (S O) i r))) *)
        rewrite Hg1.
        apply sum_powers_ortho with (q := 4*q); auto; omega.
      Qed.
  
      Let Hu1_u2_1 : u1 ⇣ u2 = 0.
      Proof.
(* Goal: @eq nat (nat_meet u1 u2) O *)
        rewrite Hu1, Hu2.
(* Goal: @eq nat (nat_meet (@msum nat nat_join O l (fun i : nat => mul (mul (b i) (c i)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat nat_join O l (fun i : nat => @msum nat nat_join O i (fun j : nat => mul (add (mul (b i) (c j)) (mul (b j) (c i))) (@mscal nat mul (S O) (add (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (S j) (S (S O)))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) O *)
        apply nat_ortho_joins.
(* Goal: forall (i j : nat) (_ : lt i m) (_ : lt j k'), @eq nat (nat_meet (mul (S O) (@mscal nat mul (S O) (mul (S (S O)) (f i)) r)) (mul (S (S O)) (@mscal nat mul (S O) j r))) O *)
        intros i j Hi Hj.
        destruct (eq_nat_dec j (2*f i)) as [ H | H ].
        + unfold r; do 2 rewrite <- power_mult.
          rewrite <- H.
(* Goal: @eq nat (nat_meet (mul (S O) (@mscal nat mul (S O) (mul j (mul (S (S (S (S O)))) q)) (S (S O)))) (mul (mul (S (S O)) (g j)) (@mscal nat mul (S O) (mul j (mul (S (S (S (S O)))) q)) (S (S O))))) O *)
          rewrite nat_meet_mult_power2.
(* Goal: @eq nat (mul (nat_meet (S O) (mul (S (S O)) (g j))) (@mscal nat mul (S O) (mul j (mul (S (S (S (S O)))) q)) (S (S O)))) O *)
          rewrite nat_meet_12n; auto.
        + rewrite nat_meet_powers_neq with (q := 4*q); auto; omega.
      Qed.

      Let Hu1_u2 : u*u = u1 ⇡ u2.
      Proof.
(* Goal: @eq nat (mul u u) (nat_join u1 u2) *)
        rewrite const_u_square.
(* Goal: @eq nat (add u1 u2) (nat_join u1 u2) *)
        apply nat_ortho_plus_join; auto.
      Qed.
   
      Let Hw_1 : w = msum nat_join 0 k' (fun i => 1*power i r).
      Proof. rewrite Hw; apply all_ones_joins; auto. Qed.

      Let H2w_1 : 2*w = msum nat_join 0 k' (fun i => 2*power i r).
      Proof. rewrite Hw; apply all_ones_2_joins; auto. Qed.

      Let Hu2_w : u2 ⇣ w = 0.
      Proof.
        rewrite Hu2, Hw_1.
        destruct (le_lt_dec k' (2*k)) as [ Hk | Hk ].
(* Goal: lt (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) q (S (S O))) *)
(* Goal: lt (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) (mul (@mscal nat mul (S O) q (S (S O))) (@mscal nat mul (S O) q (S (S O)))) *)
        2: { apply nat_ortho_joins.
(* Goal: forall (i j : nat) (_ : lt i m) (_ : lt j k'), @eq nat (nat_meet (mul (S O) (@mscal nat mul (S O) (mul (S (S O)) (f i)) r)) (mul (S (S O)) (@mscal nat mul (S O) j r))) O *)
             intros i j Hi Hj.
             rewrite nat_meet_comm.
             destruct (eq_nat_dec i j) as [ H | H ].
             + subst j; rewrite nat_meet_powers_eq with (q := 4*q); auto.
(* Goal: @eq nat (mul (nat_meet (S O) (mul (S (S O)) (g j))) (@mscal nat mul (S O) (mul j (mul (S (S (S (S O)))) q)) (S (S O)))) O *)
               rewrite nat_meet_12n; auto.
             + apply nat_meet_powers_neq with (q := 4*q); auto; try omega. }
        replace (2*k) with (k'+(2*k-k')) by omega.
        rewrite msum_plus, nat_meet_comm, nat_meet_join_distr_l, nat_join_comm; auto.
        rewrite (proj2 (nat_ortho_joins k' (2*k-k') _ _)), nat_join_0n.
(* Goal: lt (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) q (S (S O))) *)
(* Goal: lt (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) (mul (@mscal nat mul (S O) q (S (S O))) (@mscal nat mul (S O) q (S (S O)))) *)
        2: { intros i j H1 H2.
             apply nat_meet_powers_neq with (q := 4*q); auto; try omega. }
(* Goal: @eq nat (nat_meet (@msum nat nat_join O l (fun i : nat => mul (mul (b i) (c i)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat nat_join O l (fun i : nat => @msum nat nat_join O i (fun j : nat => mul (add (mul (b i) (c j)) (mul (b j) (c i))) (@mscal nat mul (S O) (add (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (S j) (S (S O)))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) O *)
        apply nat_ortho_joins.
(* Goal: forall (i j : nat) (_ : lt i m) (_ : lt j k'), @eq nat (nat_meet (mul (S O) (@mscal nat mul (S O) (mul (S (S O)) (f i)) r)) (mul (S (S O)) (@mscal nat mul (S O) j r))) O *)
        intros i j Hi Hj.
        destruct (eq_nat_dec i j) as [ H | H ].
        + subst j; rewrite nat_meet_powers_eq with (q := 4*q); auto.
(* Goal: @eq nat (mul (nat_meet (S O) (mul (S (S O)) (g j))) (@mscal nat mul (S O) (mul j (mul (S (S (S (S O)))) q)) (S (S O)))) O *)
          rewrite nat_meet_12n; auto.
        + apply nat_meet_powers_neq with (q := 4*q); auto; try omega.
      Qed.

      Fact const_u1_prefix : { q | q <= m /\ u*u ⇣ w = ∑ q (fun i => 1*power (2*f i) r) }.
      Proof.
        destruct inc_seq_split_lt with (n := m) (f := fun i => 2*f i) (k := k') as (a & H1 & H2 & H3).
        + intros i j Hij; apply Hf2 in Hij; omega.
        + exists a; split; auto.
(* Goal: iff (@eq nat p (nat_meet (mul u u) (mul (S (S O)) w))) (@eq nat p u2) *)
          rewrite Hu1_u2, nat_meet_comm, nat_meet_join_distr_l.
(* Goal: iff (@eq nat p (nat_join (nat_meet w u1) (nat_meet w u2))) (@eq nat p u1) *)
          do 2 rewrite (nat_meet_comm w).
          rewrite Hu2_w, nat_join_n0.
(* Goal: binary_le u1 w *)
          rewrite Hu1, Hw_1.
          replace m with (a+(m-a)) by omega.
          rewrite msum_plus, nat_meet_comm, nat_meet_join_distr_l.
          rewrite nat_join_comm.
          rewrite (proj2 (nat_ortho_joins k' (m-a) _ _)), nat_join_0n; auto.
          3: apply nat_join_monoid.
          * rewrite Hseq_u; auto.
            rewrite nat_meet_comm.
(* Goal: @eq nat (nat_meet u2 (mul (S (S O)) w)) u2 *)
            apply binary_le_nat_meet.
(* Goal: binary_le (@msum nat nat_join O m (fun i : nat => mul (S O) (@mscal nat mul (S O) (mul (S (S O)) (f i)) r))) (@msum nat nat_join O k' (fun i : nat => mul (S O) (@mscal nat mul (S O) i r))) *)
            apply nat_joins_binary_le.
(* Goal: forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
            intros i Hi.
            exists (2*f i); split; auto.
          * intros; apply  nat_meet_powers_neq with (q := 4*q); auto; try omega.
            generalize (H3 (a + j)); intros; omega.
      Qed. 
         
      Hypothesis (Hk : 2*k < k').

      Let Hu1_w : u1 ⇣ w = u1.
      Proof.
(* Goal: @eq nat (nat_meet u2 (mul (S (S O)) w)) u2 *)
        apply binary_le_nat_meet.
(* Goal: binary_le u1 w *)
        rewrite Hu1, Hw_1.
(* Goal: binary_le (@msum nat nat_join O m (fun i : nat => mul (S O) (@mscal nat mul (S O) (mul (S (S O)) (f i)) r))) (@msum nat nat_join O k' (fun i : nat => mul (S O) (@mscal nat mul (S O) i r))) *)
        apply nat_joins_binary_le.
(* Goal: forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
        intros i Hi.
        exists (2*f i); split; auto.
(* Goal: lt (mul (S (S O)) (f i)) k' *)
        apply le_lt_trans with (2 := Hk), mult_le_compat; auto.
      Qed.

      Let Hu1_2w : u1 ⇣ (2*w) = 0.
      Proof.
(* Goal: @eq nat (nat_meet u1 (mul (S (S O)) w)) O *)
        rewrite H2w_1, Hu1, nat_ortho_joins.
(* Goal: forall (i j : nat) (_ : lt i m) (_ : lt j k'), @eq nat (nat_meet (mul (S O) (@mscal nat mul (S O) (mul (S (S O)) (f i)) r)) (mul (S (S O)) (@mscal nat mul (S O) j r))) O *)
        intros i j Hi Hj.
        destruct (eq_nat_dec j (2 * f i)) as [ H | H ].
        + rewrite <- H, nat_meet_powers_eq with (q := 4*q); auto; try omega.
(* Goal: @eq nat (mul (nat_meet (S O) (S (S O))) (@mscal nat mul (S O) j r)) O *)
          rewrite nat_meet_12; auto.
        + apply nat_meet_powers_neq with (q := 4*q); auto; try omega.
      Qed.

      Fact const_u1_meet p : p = (u*u) ⇣ w <-> p = u1.
      Proof.
(* Goal: iff (@eq nat p (nat_meet (mul u u) (mul (S (S O)) w))) (@eq nat p u2) *)
        rewrite Hu1_u2, nat_meet_comm, nat_meet_join_distr_l.
(* Goal: iff (@eq nat p (nat_join (nat_meet w u1) (nat_meet w u2))) (@eq nat p u1) *)
        do 2 rewrite (nat_meet_comm w).
(* Goal: iff (@eq nat p (nat_join (nat_meet u1 w) (nat_meet u2 w))) (@eq nat p u1) *)
        rewrite Hu1_w, Hu2_w, nat_join_n0; tauto.
      Qed.

      Fact const_u1_eq : (u*u) ⇣ w = u1.
      Proof. apply const_u1_meet; auto. Qed.

      Hypothesis Hf : forall i, i < m -> f i = power (S i) 2.

      Let Hu2_1 : u2 = msum nat_join 0 m (fun i => msum nat_join 0 i (fun j => 2*power (f i + f j) r)).
      Proof.
(* Goal: @eq nat u2 (@msum nat nat_join O m (fun i : nat => @msum nat nat_join O i (fun j : nat => mul (S (S O)) (@mscal nat mul (S O) (add (f i) (f j)) r)))) *)
        unfold u2.
        apply double_sum_powers_ortho with (q := 4*q); auto; try omega.
        + intros; omega.
        + intros ? ? ? ? ? ?; repeat rewrite Hf; try omega.
(* Goal: forall (_ : @eq nat (@msum nat add O l (fun i : nat => mul (mul (a i) (S O)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat add O l (fun i : nat => mul (mul (b i) (c i)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
          intros E.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          apply sum_2_power_2_injective in E; omega.
      Qed.

      (* This cannot be proved anymore without stronger hypothesis on f *) 

      Let Hu2_2w : u2 ⇣ (2*w) = u2.
      Proof.
(* Goal: @eq nat (nat_meet u2 (mul (S (S O)) w)) u2 *)
        apply binary_le_nat_meet.
(* Goal: binary_le u2 (mul (S (S O)) w) *)
        rewrite H2w_1, Hu2_1.
(* Goal: binary_le (@msum nat nat_join O m (fun i : nat => @msum nat nat_join O i (fun j : nat => mul (S (S O)) (@mscal nat mul (S O) (add (f i) (f j)) r)))) (@msum nat nat_join O k' (fun i : nat => mul (S (S O)) (@mscal nat mul (S O) i r))) *)
        apply nat_double_joins_binary_le.
(* Goal: forall (i j : nat) (_ : and (lt j i) (lt i m)), @ex nat (fun k : nat => and (lt k k') (binary_le (mul (S (S O)) (@mscal nat mul (S O) (add (f i) (f j)) r)) (mul (S (S O)) (@mscal nat mul (S O) k r)))) *)
        intros i j Hij.
        exists (f i + f j); split; auto.
        apply le_lt_trans with (2*f i); auto.
        + apply Hf2 in Hij; omega.
        + apply le_lt_trans with (2 := Hk), mult_le_compat; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          apply Hf1; omega.
      Qed. 

      Fact const_u2_meet p : p = (u*u) ⇣ (2*w) <-> p = u2.
      Proof.
(* Goal: iff (@eq nat p (nat_meet (mul u u) (mul (S (S O)) w))) (@eq nat p u2) *)
        rewrite Hu1_u2, nat_meet_comm, nat_meet_join_distr_l.
        do 2 rewrite (nat_meet_comm (2*w)).
(* Goal: iff (@eq nat p (nat_join (nat_meet u1 (mul (S (S O)) w)) (nat_meet u2 (mul (S (S O)) w)))) (@eq nat p u2) *)
        rewrite Hu1_2w, Hu2_2w, nat_join_0n; tauto.
      Qed.

    End increase.

    Let Hl'' : 2*l < r.
    Proof.
(* Goal: lt (mul (S (S O)) (S m)) r *)
      unfold r.
(* Goal: lt (mul (S (S O)) l) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) *)
      rewrite (mult_comm _ q), power_mult.
(* Goal: lt (mul (S (S O)) l) (@mscal nat mul (S O) q (@mscal nat mul (S O) (S (S (S (S O)))) (S (S O)))) *)
      change (power 4 2) with 16.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      apply power_smono_l with (x := 16) in Hlq; try omega.
(* Goal: lt (mul (S (S O)) l) (@mscal nat mul (S O) q (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))) *)
      apply le_lt_trans with (2 := Hlq).
(* Goal: le (S (S O)) (@mscal nat mul (S O) (S l) (S (S O))) *)
      rewrite plus_comm; simpl plus; rewrite power_S.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      apply mult_le_compat; try omega.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      apply power_ge_n; omega.
    Qed.

    Section const_1_cn.

      (* Perhaps you should encode the predicate that 
          
           w = ∑ {i=0..2^{l+1}} r^i
           u = ∑ {1..l} r^{2^i} and u1 = u*u ⇣ w

         as diophantine and use that predicate because
         it is used for Const1 and the product and CodeNat *)

      Variable (u u1 : nat) (Hu  : u = ∑ l (fun i => power (power (S i) 2) r))
                            (Hu1 : u1 = ∑ l (fun i => power (power (S (S i)) 2) r)).
 
      Let w  := ∑ (S (power (S l) 2)) (fun i => power i r).
 (*     Let u1 := ∑ l (fun i => power (power (S (S i)) 2) r). *)
      Let u2 := ∑ l (fun i => ∑ i (fun j => 2*power (power (S i) 2 + power (S j) 2) r)).
 
      Let H18 : 1+(r-1)*w = power (S (power (S l) 2)) r.
      Proof. rewrite <- all_ones_dio; auto. Qed.

      Let H19 : u*u = u1 + u2.
      Proof.
(* Goal: divides (@mscal nat mul (S O) (S (S (S (S O)))) r) u1 *)
        rewrite Hu1. 
(* Goal: @eq nat (mul u u) (add (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) r)) u2) *)
        apply const_u_square with (w := w) (2 := eq_refl); auto.
      Qed.

      Let k := S (power (S l) 2).
      Let f i := power (S i) 2.

      Let Hf1 i : i < l -> 2*f i < k.
      Proof.
(* Goal: forall _ : lt i l, lt (mul (S (S O)) (f i)) k *)
        unfold k, f.
        intros; rewrite <- power_S; apply le_n_S, power_mono_l; omega.
      Qed.

      Let Hf2 i j : i < j < l -> f i < f j.
      Proof. intros; apply power_smono_l; omega. Qed.

      Let Hf3 i1 j1 i2 j2 : j1 <= i1 < l -> j2 <= i2 < l -> f i1 + f j1 = f i2 + f j2 -> i1 = i2 /\ j1 = j2.
      Proof.
(* Goal: forall (_ : le j1 i1) (_ : le j2 i2) (_ : @eq nat (add (@mscal nat mul (S O) i1 (S (S O))) (@mscal nat mul (S O) j1 (S (S O)))) (add (@mscal nat mul (S O) i2 (S (S O))) (@mscal nat mul (S O) j2 (S (S O))))), and (@eq nat i1 i2) (@eq nat j1 j2) *)
        unfold f; intros H1 H2 E.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        apply sum_2_power_2_injective in E; omega.
      Qed.

      Let H20 : u1 = (u*u) ⇣ w.
      Proof. 
(* Goal: @eq nat u1 (nat_meet (mul u u) w) *)
        rewrite const_u1_meet with (k := power l 2) (m := l) (f := f); auto.
        * intros i Hi; specialize (Hf1 Hi).
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          revert Hf1; unfold k; rewrite power_S; intros; omega.
        * rewrite <- power_S; auto.
      Qed. 

      Let H21 : u2 = (u*u) ⇣ (2*w).
      Proof. 
(* Goal: @eq nat u2 (nat_meet (mul u u) (mul (S (S O)) w)) *)
        rewrite const_u2_meet with (k := power l 2) (m := l) (f := f); auto.
        * intros i Hi; specialize (Hf1 Hi).
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          revert Hf1; unfold k; rewrite power_S; intros; omega.
        * rewrite <- power_S; auto.
     Qed. 
 
      Let H22 : power 2 r + u1 = u + power (power (S l) 2) r.
      Proof.
(* Goal: @eq nat (add (@mscal nat mul (S O) (S (S O)) r) u1) (add u (@mscal nat mul (S O) (@mscal nat mul (S O) (S l) (S (S O))) r)) *)
        rewrite Hu, Hu1.
(* Goal: @eq nat (add (@mscal nat mul (S O) (S (S O)) r) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) r))) (add (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) r)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S l) (S (S O))) r)) *)
        destruct l.
        + do 2 rewrite msum_0.
(* Goal: @eq nat (add (@mscal nat mul (S O) (S (S O)) r) O) (add O (@mscal nat mul (S O) (@mscal nat mul (S O) (S O) (S (S O))) r)) *)
          rewrite power_1; auto.
        + rewrite msum_plus1, msum_S; auto.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
          rewrite power_1; ring.
      Qed.
  
      Let H23 : divides (power 4 r) u1.
      Proof.
(* Goal: divides (@mscal nat mul (S O) (S (S (S (S O)))) r) u1 *)
        rewrite Hu1.
(* Goal: divides (@mscal nat mul (S O) (S (S (S (S O)))) r) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) r)) *)
        apply divides_msum.
(* Goal: forall (i : nat) (_ : lt i l), divides (@mscal nat mul (S O) (S (S (S (S O)))) r) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) r) *)
        intros i _.
(* Goal: divides (@mscal nat mul (S O) (S (S (S (S O)))) r) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) r) *)
        apply divides_power.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        apply (@power_mono_l 2 _ 2); omega.
      Qed.

      Lemma const1_cn : exists w u2,    1+(r-1)*w = power (S (power (S l) 2)) r
                                     /\ u*u = u1 + u2
                                     /\ u1 = (u*u) ⇣ w
                                     /\ u2 = (u*u) ⇣ (2*w)
                                     /\ power 2 r + u1 = u + power (power (S l) 2) r
                                     /\ divides (power 4 r) u1.
      Proof.
(* Goal: @ex nat (fun w : nat => @ex nat (fun u2 : nat => and (@eq nat (add (S O) (mul (sub r (S O)) w)) (@mscal nat mul (S O) (S (@mscal nat mul (S O) (S l) (S (S O)))) r)) (and (@eq nat (mul u u) (add u1 u2)) (and (@eq nat u1 (nat_meet (mul u u) w)) (and (@eq nat u2 (nat_meet (mul u u) (mul (S (S O)) w))) (and (@eq nat (add (@mscal nat mul (S O) (S (S O)) r) u1) (add u (@mscal nat mul (S O) (@mscal nat mul (S O) (S l) (S (S O))) r))) (divides (@mscal nat mul (S O) (S (S (S (S O)))) r) u1))))))) *)
        exists w, u2; repeat (split; auto).
      Qed.

    End const_1_cn.

    Section const_1_cs.

      Variable (w u u1 u2 : nat).

      Hypothesis (H18 : 1+(r-1)*w = power (S (power (S l) 2)) r)
                 (H19 : u*u = u1 + u2)
                 (H20 : u1 = (u*u) ⇣ w)
                 (H21 : u2 = (u*u) ⇣ (2*w))
                 (H22 : power 2 r + u1 = u + power (power (S l) 2) r)
                 (H23 : divides (power 4 r) u1).

      Let Hw_0 : w = ∑ (S (power (S l) 2)) (fun i => power i r).
      Proof. apply all_ones_dio; auto. Qed.

      Let Hw_1 : w = ∑ (S (power (S l) 2)) (fun i => 1*power i r).
      Proof. rewrite Hw_0; apply msum_ext; intros; ring. Qed.

      Let Hw : w = msum nat_join 0 (S (power (S l) 2)) (fun i => 1*power i r).
      Proof. apply all_ones_joins; auto. Qed.

      Let H2w : 2*w = msum nat_join 0 (S (power (S l) 2)) (fun i => 2*power i r).
      Proof. apply all_ones_2_joins; auto. Qed.
    
      Let Hu1_0 : u1 ≲ ∑ (S (power (S l) 2)) (fun i => 1*power i r).
      Proof. rewrite H20, <- Hw_1; auto. Qed.

(* Goal: lt (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) q (S (S O))) *)
(* Goal: lt (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) (mul (@mscal nat mul (S O) q (S (S O))) (@mscal nat mul (S O) q (S (S O)))) *)
      Let mk_full : { m : nat & { k | u1 = ∑ (S m) (fun i => power (k i) r) 
                                /\ m <= power (S l) 2
                                /\ (forall i, i < S m -> k i <= power (S l) 2) 
                                /\ forall i j, i < j < S m -> k i < k j } }.
      Proof.
(* Goal: lt (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) q (S (S O))) *)
(* Goal: lt (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) (mul (@mscal nat mul (S O) q (S (S O))) (@mscal nat mul (S O) q (S (S O)))) *)
        assert ({ k : nat &
                 { g : nat -> nat & 
                 { h | u1 = ∑ k (fun i => g i * power (h i) r)
                     /\ k <= S (power (S l) 2)
                     /\ (forall i, i < k -> g i <> 0 /\ g i ≲ 1)
                     /\ (forall i, i < k -> h i < S (power (S l) 2))
                     /\ (forall i j, i < j < k -> h i < h j) } } }) as H.
(* Goal: lt (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) q (S (S O))) *)
(* Goal: lt (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) (mul (@mscal nat mul (S O) q (S (S O))) (@mscal nat mul (S O) q (S (S O)))) *)
        { apply (@sum_powers_binary_le_inv _ Hq' r eq_refl _ (fun _ => _) (fun i => i)); auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          intros; omega. }
(* Goal: @sigT nat (fun m : nat => @sig (forall _ : nat, nat) (fun k : forall _ : nat, nat => and (@eq nat u1 (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (k i) r))) (and (le m (@mscal nat mul (S O) (S l) (S (S O)))) (and (forall (i : nat) (_ : lt i (S m)), le (k i) (@mscal nat mul (S O) (S l) (S (S O)))) (forall (i j : nat) (_ : and (lt i j) (lt j (S m))), lt (k i) (k j)))))) *)
        destruct H as (m' & g & h & H1 & H2 & H3 & H4 & H5).
        assert (H6 : forall i, i < m' -> g i = 1).
(* Goal: lt (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) q (S (S O))) *)
(* Goal: lt (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) (mul (@mscal nat mul (S O) q (S (S O))) (@mscal nat mul (S O) q (S (S O)))) *)
        { intros i Hi; generalize (H3 _ Hi).
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          intros (? & G2); apply binary_le_le in G2; omega. }
        assert (H7 : u1 = ∑ m' (fun i => 1 * power (h i) r)).
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        { rewrite H1; apply msum_ext; intros; rewrite H6; try ring; omega. }
(* Goal: @sigT nat (fun m : nat => @sig (forall _ : nat, nat) (fun k : forall _ : nat, nat => and (@eq nat u1 (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (k i) r))) (and (le m (@mscal nat mul (S O) (S l) (S (S O)))) (and (forall (i : nat) (_ : lt i (S m)), le (k i) (@mscal nat mul (S O) (S l) (S (S O)))) (forall (i j : nat) (_ : and (lt i j) (lt j (S m))), lt (k i) (k j)))))) *)
        assert (H8 : u1 = ∑ m' (fun i => power (h i) r)).
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
        { rewrite H7; apply msum_ext; intros; ring. }
(* Goal: @sigT nat (fun m : nat => @sig (forall _ : nat, nat) (fun k : forall _ : nat, nat => and (@eq nat u1 (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (k i) r))) (and (le m (@mscal nat mul (S O) (S l) (S (S O)))) (and (forall (i : nat) (_ : lt i (S m)), le (k i) (@mscal nat mul (S O) (S l) (S (S O)))) (forall (i j : nat) (_ : and (lt i j) (lt j (S m))), lt (k i) (k j)))))) *)
        assert (H9 : m' <> 0).
(* Goal: lt (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) q (S (S O))) *)
(* Goal: lt (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) (mul (@mscal nat mul (S O) q (S (S O))) (@mscal nat mul (S O) q (S (S O)))) *)
        { intros E; rewrite E, msum_0 in H1.
(* Goal: False *)
          assert (power 2 r < power (power (S l) 2) r) as C.
(* Goal: lt (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) q (S (S O))) *)
(* Goal: lt (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) (mul (@mscal nat mul (S O) q (S (S O))) (@mscal nat mul (S O) q (S (S O)))) *)
          { apply power_smono_l; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
            apply (@power_smono_l 1 _ 2); omega. }
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          omega. }
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        destruct m' as [ | m ]; try omega.
(* Goal: @sigT nat (fun m : nat => @sig (forall _ : nat, nat) (fun k : forall _ : nat, nat => and (@eq nat u1 (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (k i) r))) (and (le m (@mscal nat mul (S O) (S l) (S (S O)))) (and (forall (i : nat) (_ : lt i (S m)), le (k i) (@mscal nat mul (S O) (S l) (S (S O)))) (forall (i j : nat) (_ : and (lt i j) (lt j (S m))), lt (k i) (k j)))))) *)
        exists m, h; repeat (split; auto).
        + omega.
        + intros i; generalize (H4 i); intros; omega.
      Qed.

      Let m := projT1 mk_full.
      Let k := proj1_sig (projT2 mk_full).

      Let Hu1 : u1 = ∑ (S m) (fun i => power (k i) r).        Proof. apply (proj2_sig (projT2 mk_full)). Qed.
      Let Hm : m <= (power (S l) 2).                          Proof. apply (proj2_sig (projT2 mk_full)). Qed.
      Let Hk1 : forall i, i < S m -> k i <= power (S l) 2.    Proof. apply (proj2_sig (projT2 mk_full)). Qed.
      Let Hk2 : forall i j, i < j < S m -> k i < k j.         Proof. apply (proj2_sig (projT2 mk_full)). Qed.

      Let Hh_0 : 4 <= k 0.
      Proof.
(* Goal: le (S (S (S (S O)))) (k O) *)
        rewrite Hu1 in H23.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        apply power_divides_sum_power in H23; auto; try omega.
      Qed.

      Let f1 i := match i with 0 => 2 | S i => k i end.
      Let f2 i := if le_lt_dec i m then power (S l) 2 else k i.

      Let Hf1_0 : forall i, i <= S m -> f1 i < S (power (S l) 2).
      Proof.
(* Goal: forall (i : nat) (_ : le i (S m)), lt (f1 i) (S (@mscal nat mul (S O) (S l) (S (S O)))) *)
        intros [ | i ] Hi; simpl; apply le_n_S.
        + rewrite power_S.
          change 2 with (2*1) at 1.
(* Goal: le (mul (S (S O)) (S (@mscal nat mul (S O) (S l) (S (S O))))) (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) *)
          apply mult_le_compat; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          apply power_ge_1; omega.
        + apply Hk1; auto.
      Qed.

      Let Hf1_1 : forall i j, i < j <= S m -> f1 i < f1 j.
      Proof.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        intros [ | i ] [ | j ] Hij; simpl; try omega.
        * apply lt_le_trans with (k 0); try omega.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          destruct j; auto; apply lt_le_weak, Hk2; omega.
        * apply Hk2; omega.
      Qed.

      Let Hf1_2 : ∑ (S (S m)) (fun i => power (f1 i) r) = u + power (power (S l) 2) r.
      Proof.
(* Goal: @eq nat (@msum nat add O (S (S m)) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) (add u (@mscal nat mul (S O) (@mscal nat mul (S O) (S l) (S (S O))) r)) *)
        rewrite msum_S; unfold f1.
        rewrite <- Hu1; auto.
      Qed.

      Let Hh_1 : k m = power (S l) 2.
      Proof.
(* Goal: @eq nat (k m) (@mscal nat mul (S O) (S l) (S (S O))) *)
        destruct (le_lt_dec (power (S l) 2) (k m)) as [ H | H ].
        + apply le_antisym; auto.
        + assert (∑ (S (S m)) (fun i => power (f1 i) r) < power (power (S l) 2) r); try omega.
(* Goal: lt (@msum nat add O (S (S m)) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S l) (S (S O))) r) *)
          apply sum_powers_inc_lt; auto.
          - intros [ | i ] Hi; simpl.
            * apply (@power_smono_l 1 _ 2); omega.
            * apply le_lt_trans with (2 := H).
(* Goal: le (k i) (k m) *)
              destruct (eq_nat_dec i m); subst; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
              apply lt_le_weak, Hk2; omega.
          - intros; apply Hf1_1; omega.
      Qed.
 
      Let Hu : u = ∑ (S m) (fun i => power (f1 i) r).
      Proof.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        rewrite msum_plus1 in Hf1_2; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        simpl f1 at 2 in Hf1_2.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        rewrite Hh_1 in Hf1_2.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        omega.
      Qed.
        
      Let Huu : u*u = ∑ (S m) (fun i => power (2*f1 i) r)
                    + ∑ (S m) (fun i => ∑ i (fun j => 2*power (f1 i + f1 j) r)).
      Proof.
(* Goal: @eq nat (mul u u) (add (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (mul (S (S O)) (f1 i)) r)) (@msum nat add O (S m) (fun i : nat => @msum nat add O i (fun j : nat => mul (S (S O)) (@mscal nat mul (S O) (add (f1 i) (f1 j)) r))))) *)
        rewrite Hu, square_sum; f_equal.
        + apply msum_ext; intros; rewrite <- power_plus; f_equal; omega.
        + rewrite <- sum_0n_scal_l; apply msum_ext; intros i Hi.
          rewrite <- sum_0n_scal_l; apply msum_ext; intros j Hj.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
          rewrite power_plus; ring.
      Qed.

      (* This one should not be that hard given S l < q but to check *)

      Let HSl_q : 2 * S (power (S l) 2) < power (2 * q) 2.
      Proof.
        rewrite <- (mult_2_eq_plus q), power_plus.
        apply le_lt_trans with (2*power q 2).
(* Goal: le (mul (S (S O)) (S (@mscal nat mul (S O) (S l) (S (S O))))) (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) *)
        + apply mult_le_compat; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          apply power_smono_l; omega.
        + assert (power 1 2 < power q 2) as H.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          { apply power_smono_l; omega. }
(* Goal: lt (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) (mul (@mscal nat mul (S O) q (S (S O))) (@mscal nat mul (S O) q (S (S O)))) *)
          rewrite power_1 in H.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          apply Nat.mul_lt_mono_pos_r; omega.
      Qed.
  
      Let Hu1_1 : { d | d <= S m /\ u1 = ∑ d (fun i => power (2*f1 i) r) }.
      Proof.
        destruct const_u1_prefix with (m := S m) (k := power (S l) 2) (k' := S (power (S l) 2))
           (u := u) (w := w) (f := fun i => f1 i)
           as (d & H1 & H2); auto.
        + unfold r.
          apply le_lt_trans with (2*S (power (S l) 2)); try omega.
(* Goal: lt (mul (S (S O)) (S (@mscal nat mul (S O) (S l) (S (S O))))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) *)
          apply le_lt_trans with (power (S (S (S l))) 2).
(* Goal: le (S (S O)) (@mscal nat mul (S O) (S l) (S (S O))) *)
          do 4 rewrite power_S.
          * generalize (@power_ge_1 l 2); intros; omega.
          * apply power_smono_l; omega.
        + intros i Hi; generalize (@Hf1_0 i); intros; omega.
        + intros; apply Hf1_1; omega.
        + exists d; split; auto.
(* Goal: @eq nat u1 (@msum nat add O d (fun i : nat => @mscal nat mul (S O) (mul (S (S O)) (f1 i)) r)) *)
          rewrite H20, H2.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
          apply msum_ext; intros; ring.
      Qed.

      Let Hk_final : k 0 = 4 /\ forall i, i < m -> k (S i) = 2*k i.
      Proof.
(* Goal: and (@eq nat (k O) (S (S (S (S O))))) (forall (i : nat) (_ : lt i m), @eq nat (k (S i)) (mul (S (S O)) (k i))) *)
        destruct Hu1_1 as (d & Hd1 & E).
(* Goal: and (@eq nat (k O) (S (S (S (S O))))) (forall (i : nat) (_ : lt i m), @eq nat (k (S i)) (mul (S (S O)) (k i))) *)
        rewrite Hu1 in E.
(* Goal: and (@eq nat (k O) (S (S (S (S O))))) (forall (i : nat) (_ : lt i m), @eq nat (k (S i)) (mul (S (S O)) (k i))) *)
        apply sum_powers_injective in E; auto.
        + destruct E as (? & E); subst d; split.
          * rewrite E; try omega; auto.
          * intros; rewrite E; auto; omega.
        + intros i j H; specialize (@Hf1_1 i j); intros; omega.
      Qed.

      Let Hk_is_power i : i <= m -> k i = power (S (S i)) 2.
      Proof.
(* Goal: forall _ : le i m, @eq nat (k i) (@mscal nat mul (S O) (S (S i)) (S (S O))) *)
         induction i as [ | i IHi ]; intros Hi.
         + rewrite (proj1 Hk_final); auto.
         + rewrite (proj2 Hk_final), IHi, <- power_S; auto; omega.
      Qed.

      Let Hm_is_l : S m = l.
      Proof.
(* Goal: @eq nat (S m) l *)
        rewrite Hk_is_power in Hh_1; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        apply power_2_inj in Hh_1; omega.
      Qed.
        
      Fact obtain_u_u1_value :  u  = ∑ l (fun i => power (power (S i) 2) r)
                             /\ u1 = ∑ l (fun i => power (power (S (S i)) 2) r).
      Proof.
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
        split.
        + rewrite <- Hm_is_l, Hu.
(* Goal: @eq nat (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (k i) r)) (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) r)) *)
          apply msum_ext.
(* Goal: forall (i : nat) (_ : lt i (S m)), @eq nat (@mscal nat mul (S O) (k i) r) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) r) *)
          intros [ | i ]; simpl; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          intros; rewrite Hk_is_power; auto; omega.
        + rewrite <- Hm_is_l, Hu1.
(* Goal: @eq nat (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (k i) r)) (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) r)) *)
          apply msum_ext.
(* Goal: forall (i : nat) (_ : lt i (S m)), @eq nat (@mscal nat mul (S O) (k i) r) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) r) *)
          intros [ | i ]; simpl; auto.
          * rewrite Hk_is_power; auto; omega.
          * intros; rewrite Hk_is_power; auto; omega.
      Qed.

    End const_1_cs.

  End const_1.

  Variable (l q : nat).

  Notation r := (power (4*q) 2).

  Definition seqs_of_ones u u1 :=
                   l+1 < q 
                /\ u  = ∑ l (fun i => power (power (S i) 2) r)
                /\ u1 = ∑ l (fun i => power (power (S (S i)) 2) r).

  (* This lemma shows that seqs_of_ones can be encoded by a diophantine expression *)

  Lemma seqs_of_ones_dio u u1 :
            seqs_of_ones u u1 
        <-> l = 0 /\ u = 0 /\ u1 = 0 /\ 2 <= q
         \/ 0 < l /\ l+1 < q
         /\ exists u2 w r0 r1 p1 p2,
                r0 = r 
             /\ r1+1 = r0
             /\ p1 = power (1+l) 2
             /\ p2 = power p1 r0
             /\ 1+r1*w = r0*p2
             /\ u*u = u1 + u2
             /\ u1 = (u*u) ⇣ w
             /\ u2 = (u*u) ⇣ (2*w)
             /\ r0*r0 + u1 = u + p2
             /\ divides (r0*r0*r0*r0) u1. 
  Proof.
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
    split.
    + intros (H2 & H3 & H4).
(* Goal: or (and (@eq nat l O) (and (@eq nat u O) (and (@eq nat u1 O) (le (S (S O)) q)))) (and (lt O l) (and (lt (add l (S O)) q) (@ex nat (fun u2 : nat => @ex nat (fun w : nat => @ex nat (fun r0 : nat => @ex nat (fun r1 : nat => @ex nat (fun p1 : nat => @ex nat (fun p2 : nat => and (@eq nat r0 (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat (add r1 (S O)) r0) (and (@eq nat p1 (@mscal nat mul (S O) (add (S O) l) (S (S O)))) (and (@eq nat p2 (@mscal nat mul (S O) p1 r0)) (and (@eq nat (add (S O) (mul r1 w)) (mul r0 p2)) (and (@eq nat (mul u u) (add u1 u2)) (and (@eq nat u1 (nat_meet (mul u u) w)) (and (@eq nat u2 (nat_meet (mul u u) (mul (S (S O)) w))) (and (@eq nat (add (mul r0 r0) u1) (add u p2)) (divides (mul (mul (mul r0 r0) r0) r0) u1)))))))))))))))))) *)
      destruct (le_lt_dec l 0) as [ H1 | H1 ].
      - assert (l=0) by omega; subst l.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        rewrite msum_0 in H3, H4; subst; left; omega.
      - right; split; auto; split; auto.
(* Goal: @ex nat (fun u2 : nat => @ex nat (fun w : nat => @ex nat (fun r0 : nat => @ex nat (fun r1 : nat => @ex nat (fun p1 : nat => @ex nat (fun p2 : nat => and (@eq nat r0 (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat (add r1 (S O)) r0) (and (@eq nat p1 (@mscal nat mul (S O) (add (S O) l) (S (S O)))) (and (@eq nat p2 (@mscal nat mul (S O) p1 r0)) (and (@eq nat (add (S O) (mul r1 w)) (mul r0 p2)) (and (@eq nat (mul u u) (add u1 u2)) (and (@eq nat u1 (nat_meet (mul u u) w)) (and (@eq nat u2 (nat_meet (mul u u) (mul (S (S O)) w))) (and (@eq nat (add (mul r0 r0) u1) (add u p2)) (divides (mul (mul (mul r0 r0) r0) r0) u1))))))))))))))) *)
        destruct (const1_cn H1 H2 H3 H4) as (w & u2 & E1 & E2 & E3 & E4 & E5 & E6).
        exists u2, w, r, (r-1), (power (S l) 2), (power (power (S l) 2) r); repeat (split; auto).
        * generalize (@power_ge_1 (4*q) 2); intros; omega.
        * revert E5; rewrite power_S, power_1; auto.
        * revert E6; do 3 rewrite power_S; rewrite power_1.
(* Goal: divides (mul (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (mul (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (mul (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) u1 *)
          repeat rewrite mult_assoc; auto.
    + intros [ (H1 & H2 & H3 & H4)
             | (H1 & H2 & u2 & w & r0 & r1 & p1 & p2 & ? & H0 & ? & ? & E1 & E2 & E3 & E4 & E5 & E6) ].
      - red; subst; do 2 rewrite msum_0; omega.
      - assert (r1 = r0-1) by omega; clear H0.
(* Goal: is_digit (@msum nat add O (S n) (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) p (f i) (a i) *)
        subst r0 r1 p1 p2; split; auto.
(* Goal: and (@eq nat u (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@eq nat u1 (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) *)
        apply obtain_u_u1_value with w u2; auto.
        * rewrite power_S, power_1; auto.
        * do 3 rewrite power_S; rewrite power_1.
(* Goal: divides (mul (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (mul (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (mul (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) u1 *)
          repeat rewrite mult_assoc; auto.
  Qed.

  Definition is_cipher_of f a :=
                 l+1 < q
              /\ (forall i, i < l -> f i < power q 2)
              /\ a = ∑ l (fun i => f i * power (power (S i) 2) r).

  Fact is_cipher_of_0 f a : l = 0 -> is_cipher_of f a <-> 1 < q /\ a = 0.
  Proof.
(* Goal: forall _ : @eq nat l O, iff (is_cipher_of f a) (and (lt (S O) q) (@eq nat a O)) *)
    intros ?; unfold is_cipher_of; subst l.
(* Goal: iff (and (lt (add O (S O)) q) (and (forall (i : nat) (_ : lt i O), lt (f i) (@mscal nat mul (S O) q (S (S O)))) (@eq nat a (@msum nat add O O (fun i : nat => mul (f i) (@mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))))) (and (lt (S O) q) (@eq nat a O)) *)
    rewrite msum_0; simpl.
(* Goal: iff (and (lt (S O) q) (and (forall (i : nat) (_ : lt i O), lt (f i) (@mscal nat mul (S O) q (S (S O)))) (@eq nat a O))) (and (lt (S O) q) (@eq nat a O)) *)
    repeat (split; try tauto).
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
    intros; omega.
  Qed.

  Fact is_cipher_of_inj f1 f2 a : is_cipher_of f1 a -> is_cipher_of f2 a -> forall i, i < l -> f1 i = f2 i.
  Proof.
(* Goal: forall (_ : is_cipher_of f1 a) (_ : is_cipher_of f2 a) (i : nat) (_ : lt i l), @eq nat (f1 i) (f2 i) *)
    intros (H1 & H2 & H3) (_ & H4 & H5).
(* Goal: forall (i : nat) (_ : lt i l), @eq nat (f1 i) (f2 i) *)
    rewrite H3 in H5.
(* Goal: forall (i : nat) (_ : lt i l), @eq nat (f1 i) (f2 i) *)
    revert H5; apply power_decomp_unique.
    + apply (@power_mono_l 1 _ 2); omega.
    + intros; apply power_smono_l; omega.
    + intros i Hi; apply lt_le_trans with (1 := H2 _ Hi), power_mono_l; omega.
    + intros i Hi; apply lt_le_trans with (1 := H4 _ Hi), power_mono_l; omega.
  Qed.

  Fact is_cipher_of_fun f1 f2 a b : 
          (forall i, i < l -> f1 i = f2 i)
        -> is_cipher_of f1 a 
        -> is_cipher_of f2 b
        -> a = b.
  Proof.
(* Goal: forall (_ : forall (i : nat) (_ : lt i l), @eq nat (f1 i) (f2 i)) (_ : is_cipher_of f1 a) (_ : is_cipher_of f2 b), @eq nat a b *)
    intros H1 (_ & _ & H2) (_ & _ & H3); subst a b.
(* Goal: @eq nat (@msum nat add O l (fun i : nat => mul (f1 i) (@mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat add O l (fun i : nat => mul (f2 i) (@mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) *)
    apply msum_ext; intros; f_equal; auto.
  Qed.

  Lemma is_cipher_of_equiv f1 f2 a b : 
           is_cipher_of f1 a 
        -> is_cipher_of f2 b
        -> a = b <-> forall i, i < l -> f1 i = f2 i.
  Proof.
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
    intros Ha Hb; split.
    + intro; subst; revert Ha Hb; apply is_cipher_of_inj.
    + intro; revert Ha Hb; apply is_cipher_of_fun; auto.
  Qed.

  Lemma is_cipher_of_const_1 u : 0 < l -> is_cipher_of (fun _ => 1) u
                                     <-> l+1 < q /\ exists u1, seqs_of_ones u u1.
  Proof.
(* Goal: forall _ : lt O l, iff (is_cipher_of (fun _ : nat => S O) u) (and (lt (add l (S O)) q) (@ex nat (fun u1 : nat => seqs_of_ones u u1))) *)
    intros Hl.
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
    split.
    + intros (H1 & H2 & H3); split; auto.
(* Goal: @ex nat (fun u1 : nat => seqs_of_ones u u1) *)
      exists (∑ l (fun i => power (power (S (S i)) 2) r)).
(* Goal: is_digit (@msum nat add O (S n) (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) p (f i) (a i) *)
      rewrite H3; split; auto; split; auto.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
      apply msum_ext; intros; ring.
    + intros (H1 & u1 & _ & H2).
(* Goal: is_cipher_of (fun _ : nat => S O) u *)
      apply proj1 in H2.
(* Goal: and (seqs_of_ones (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (and (@eq nat (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) (@eq nat (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (nat_meet (mul cb cc) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))))) *)
      repeat (split; auto).
      * intros; apply (@power_smono_l 0); omega.
      * rewrite H2; apply msum_ext; intros; ring.
  Qed.

  Fact is_cipher_of_u : l+1 < q -> is_cipher_of (fun _ => 1) (∑ l (fun i => power (power (S i) 2) r)).
  Proof.
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
    intros H; split; auto; split.
    + intros; apply (@power_mono_l 1 _ 2); omega.
    + apply msum_ext; intros; omega.
  Qed.
 (*
  Fact is_cipher_of_u1 : l+1 < q -> is_cipher_of (fun _ => 1) (∑ l (fun i => power (power (S (S i)) 2) r)).
  Proof.
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
    intros H; split; auto; split.
    + intros; apply (@power_mono_l 1 _ 2); omega.
    + apply msum_ext; intros; omega.
  Qed.
 *)

  Definition the_cipher f : l+1 < q -> (forall i, i < l -> f i < power q 2) -> { c | is_cipher_of f c }.
  Proof.
(* Goal: forall (_ : lt (add l (S O)) q) (_ : forall (i : nat) (_ : lt i l), lt (f i) (@mscal nat mul (S O) q (S (S O)))), @sig nat (fun c : nat => is_cipher_of f c) *)
    intros H1 H2.
    exists (∑ l (fun i => f i * power (power (S i) 2) r)); split; auto.
  Qed.

  Definition Code a := exists f, is_cipher_of f a.

  Lemma Code_dio a : Code a <-> l = 0 /\ 1 < q /\ a = 0
                             \/ 0 < l /\ l+1 < q /\ exists p u u1, p+1 = power q 2 /\ seqs_of_ones u u1 /\ a ≲ p*u.
  Proof.
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
    split.
    + intros (f & H1 & H2 & H3).
(* Goal: or (and (@eq nat l O) (and (lt (S O) q) (@eq nat v O))) (and (lt O l) (and (lt (add l (S O)) q) (@ex nat (fun p : nat => @ex nat (fun u : nat => @ex nat (fun u1 : nat => and (@eq nat p (@mscal nat mul (S O) q (S (S O)))) (and (lt c p) (and (seqs_of_ones u u1) (@eq nat v (mul c u)))))))))) *)
      destruct (eq_nat_dec l 0) as [ Hl | Hl ].
      * left; subst l; rewrite msum_0 in H3; omega.
      * right; split; try omega; split; auto.
        exists (power q 2-1), (∑ l (fun i => power (power (S i) 2) r)), (∑ l (fun i => power (power (S (S i)) 2) r)).
(* Goal: and (seqs_of_ones (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (and (@eq nat (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) (@eq nat (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (nat_meet (mul cb cc) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))))) *)
        repeat (split; auto).
        - generalize (@power_ge_1 q 2); intros; omega.
        - rewrite H3.
          apply sum_power_binary_lt with (q := 4*q); auto; try omega.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          intros; apply power_smono_l; omega.
    + intros [ (H1 & H2 & H3) | (H1 & H2 & p & u1 & u2 & ? & H3 & H4) ].
      * exists (fun _ => 0); subst a; apply is_cipher_of_0; auto.
      * destruct H3 as (_ & H3 & _).
        assert (p = power q 2 -1) by omega; subst p.
(* Goal: forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
        rewrite H3 in H4. 
        apply sum_power_binary_lt_inv with (q := 4*q) (e := fun i => power (S i) 2) in H4; auto; try omega.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        2,3: intros; apply power_smono_l; omega.
        destruct H4 as (f & H4 & H5).
(* Goal: is_digit (@msum nat add O (S n) (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) p (f i) (a i) *)
        exists f; split; auto.
  Qed.

  Definition Const c v := exists f, is_cipher_of f v /\ forall i, i < l -> f i = c.

  Lemma Const_dio c v : Const c v <-> l = 0 /\ 1 < q /\ v = 0
                                   \/ 0 < l /\ l+1 < q /\
                                      exists p u u1, p = power q 2 /\ c < p /\ seqs_of_ones u u1 /\ v = c*u.
  Proof.
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
    split.
    + intros (f & (H1 & H2 & H3) & H4).
(* Goal: or (and (@eq nat l O) (and (lt (S O) q) (@eq nat v O))) (and (lt O l) (and (lt (add l (S O)) q) (@ex nat (fun p : nat => @ex nat (fun u : nat => @ex nat (fun u1 : nat => and (@eq nat p (@mscal nat mul (S O) q (S (S O)))) (and (lt c p) (and (seqs_of_ones u u1) (@eq nat v (mul c u)))))))))) *)
      destruct (eq_nat_dec l 0) as [ Hl | Hl ].
      * left; subst l; rewrite msum_0 in H3; omega.
      * right; split; try omega; split; auto.
(* Goal: @ex nat (fun p : nat => @ex nat (fun u : nat => @ex nat (fun u1 : nat => and (@eq nat p (@mscal nat mul (S O) q (S (S O)))) (and (lt c p) (and (seqs_of_ones u u1) (@eq nat v (mul c u))))))) *)
        exists (power q 2), (∑ l (fun i => power (power (S i) 2) r)), (∑ l (fun i => power (power (S (S i)) 2) r)).
(* Goal: and (seqs_of_ones (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (and (@eq nat (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) (@eq nat (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (nat_meet (mul cb cc) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))))) *)
        repeat (split; auto).
        - rewrite <- (H4 0); try omega; apply H2; omega.
        - rewrite H3, <- sum_0n_scal_l; apply msum_ext.
(* Goal: forall (i : nat) (_ : lt i l), @eq nat (mul (f i) (@mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))) (mul c (@mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))) *)
          intros; f_equal; auto.
    + intros [ (H1 & H2 & H3) | (H1 & H2 & p & u1 & u2 & ? & H3 & H4 & H5) ].
      * exists (fun _ => 0); subst v; split.
        - apply is_cipher_of_0; auto.
        - subst l; intros; omega.
      * destruct H4 as (_ & H4 & _).
        rewrite H4, <- sum_0n_scal_l in H5.
(* Goal: is_digit (@msum nat add O (S n) (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) p (f i) (a i) *)
        exists (fun _ => c); split; auto.
(* Goal: is_digit (@msum nat add O (S n) (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) p (f i) (a i) *)
        split; auto; split; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
        intros; omega.
  Qed.

  Let Hr : 1 < q -> 4 <= r. 
  Proof.
(* Goal: forall _ : @eq nat (add (S O) (mul (sub r (S O)) w)) (@mscal nat mul (S O) l r), @eq nat w (@msum nat add O l (fun i : nat => @mscal nat mul (S O) i r)) *)
    intros H.
    replace (4*q) with (2*q+2*q) by omega.
(* Goal: lt (mul u v) (@mscal nat mul (S O) (add k k) (S (S O))) *)
    rewrite power_plus.
    change 4 with ((power 1 2)*(power 1 2)); apply mult_le_compat;
(* Goal: le (@mscal nat mul (S O) (S (f n)) r) (@mscal nat mul (S O) p r) *)
    apply power_mono_l; try omega.
  Qed.

  Section plus.

    Variable (a b c : nat-> nat) (ca cb cc : nat) 
             (Ha : is_cipher_of a ca)
             (Hb : is_cipher_of b cb) 
             (Hc : is_cipher_of c cc).

    Definition Code_plus := ca = cb + cc.
 
    Lemma Code_plus_spec : Code_plus <-> forall i, i < l -> a i = b i + c i.
    Proof.
(* Goal: iff Code_plus (forall (i : nat) (_ : lt i l), @eq nat (a i) (add (b i) (c i))) *)
      symmetry; unfold Code_plus.
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (add (b i) (c i))) (@eq nat ca (add cb cc)) *)
      destruct Ha as (H & Ha1 & Ha2).
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      destruct Hb as (_ & Hb1 & Hb2).
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      destruct Hc as (_ & Hc1 & Hc2).
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      destruct (eq_nat_dec l 0) as [ | Hl ].
      + subst l; rewrite msum_0 in *; split; intros; omega.
      + rewrite Hc2, Ha2, Hb2, <- sum_0n_distr_in_out.
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
        split.
        * intros; apply msum_ext; intros; f_equal; auto.
        * intros E i Hi. 
(* Goal: @eq nat (a i) (add (b i) (c i)) *)
          apply power_decomp_unique with (i := i) in E; auto; try omega; clear i Hi.
          - intros; apply power_smono_l; omega.
          - intros i Hi; apply lt_le_trans with (1 := Ha1 _ Hi), power_mono_l; omega.
          - intros i Hi.
(* Goal: lt (add (b i) (c i)) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) *)
            apply lt_le_trans with (power (S q) 2).
            ++ rewrite power_S, <- mult_2_eq_plus.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
               generalize (Hb1 _ Hi) (Hc1 _ Hi); omega.
(* Goal: le (@mscal nat mul (S O) (S q) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) *)
            ++ apply power_mono_l; omega.
    Qed.

  End plus.

  Notation u := (∑ l (fun i => power (power (S i) 2) r)).
  Notation u1 := (∑ l (fun i => power (power (S (S i)) 2) r)).

  Section mult_utils.
 
    Variable (b c : nat-> nat) (cb cc : nat) 
             (Hb : is_cipher_of b cb) 
             (Hc : is_cipher_of c cc).

    Let eq1 :    cb*cc = ∑ l (fun i => (b i*c i)*power (power (S (S i)) 2) r)
                       + ∑ l (fun i => ∑ i (fun j => (b i*c j + b j*c i)*power (power (S i) 2 + power (S j) 2) r)).
    Proof.
(* Goal: @eq nat (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat nat_join O l (fun i : nat => mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) *)
      destruct Hb as (H1 & Hb1 & Hb2).
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      destruct Hc as (_ & Hc1 & Hc2).
(* Goal: @eq nat (mul cb cc) (add (@msum nat add O l (fun i : nat => mul (mul (b i) (c i)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat add O l (fun i : nat => @msum nat add O i (fun j : nat => mul (add (mul (b i) (c j)) (mul (b j) (c i))) (@mscal nat mul (S O) (add (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (S j) (S (S O)))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) *)
      rewrite Hb2, Hc2, product_sums; f_equal.
      * apply msum_ext; intros; rewrite (power_S (S _)).
        rewrite <- (mult_2_eq_plus (power _ _)), power_plus; ring.
      * apply msum_ext; intros i Hi.
(* Goal: forall (i0 : nat) (_ : lt i0 (sub n i)), @eq nat (mul (a (add (S i) i0)) (@mscal nat mul (S O) (f (add (S i) i0)) p)) (mul (Nat.mul p (@mscal nat mul (S O) (f i) p)) (mul (a (add (S i) i0)) (@mscal nat mul (S O) (sub (sub (f (add (S i) i0)) (f i)) (S O)) p))) *)
        apply msum_ext; intros j Hj.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
        rewrite power_plus; ring.
    Qed.

    Let Hbc_1 i : i < l -> b i * c i < r.
    Proof.
(* Goal: @eq nat (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat nat_join O l (fun i : nat => mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) *)
      destruct Hb as (H1 & Hb1 & Hb2).
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      destruct Hc as (_ & Hc1 & Hc2).
(* Goal: forall _ : lt i l, lt (mul (b i) (c i)) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) *)
      intro; apply mult_lt_power_2_4; auto.
    Qed.
  
    Let Hbc_2 i j : i < l -> j < l -> b i * c j + b j * c i < r.
    Proof.
(* Goal: @eq nat (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat nat_join O l (fun i : nat => mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) *)
      destruct Hb as (H1 & Hb1 & Hb2).
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      destruct Hc as (_ & Hc1 & Hc2).
(* Goal: forall (_ : lt i l) (_ : lt j l), lt (add (mul (b i) (c j)) (mul (b j) (c i))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) *)
      intros; apply mult_lt_power_2_4'; auto.
    Qed.

    Let Hbc_3 : ∑ l (fun i => (b i*c i)*power (power (S (S i)) 2) r) 
              = msum nat_join 0 l (fun i => (b i*c i)*power (power (S (S i)) 2) r).
    Proof.
(* Goal: @eq nat (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat nat_join O l (fun i : nat => mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) *)
      destruct Hb as (H1 & Hb1 & Hb2).
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      destruct Hc as (_ & Hc1 & Hc2).
      apply sum_powers_ortho with (q := 4*q); try omega; auto.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      intros ? ? ? ? E; apply power_2_inj in E; omega.
    Qed.

    Let Hbc_4 : ∑ l (fun i => ∑ i (fun j => (b i*c j + b j*c i)*power (power (S i) 2 + power (S j) 2) r))
              = msum nat_join 0 l (fun i => 
                           msum nat_join 0 i (fun j => (b i*c j + b j*c i)*power (power (S i) 2 + power (S j) 2) r)).
    Proof.
(* Goal: @eq nat (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat nat_join O l (fun i : nat => mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) *)
      destruct Hb as (H1 & Hb1 & Hb2).
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      destruct Hc as (_ & Hc1 & Hc2).
      rewrite double_sum_powers_ortho with (q := 4*q); auto; try omega.
      + intros; apply Hbc_2; omega.
      + intros ? ? ? ? ? ? E; apply sum_2_power_2_injective in E; omega.
    Qed.
    
    Let eq2 :   cb*cc = msum nat_join 0 l (fun i => (b i*c i)*power (power (S (S i)) 2) r)
                      ⇡ msum nat_join 0 l (fun i => 
                           msum nat_join 0 i (fun j => (b i*c j + b j*c i)*power (power (S i) 2 + power (S j) 2) r)).
    Proof.
(* Goal: @eq nat (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat nat_join O l (fun i : nat => mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) *)
      destruct Hb as (H1 & Hb1 & Hb2).
(* Goal: @eq nat (mul cb cc) (nat_join (@msum nat nat_join O l (fun i : nat => mul (mul (b i) (c i)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat nat_join O l (fun i : nat => @msum nat nat_join O i (fun j : nat => mul (add (mul (b i) (c j)) (mul (b j) (c i))) (@mscal nat mul (S O) (add (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (S j) (S (S O)))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) *)
      rewrite eq1, Hbc_3, Hbc_4.
(* Goal: @eq nat (add (@msum nat nat_join O l (fun i : nat => mul (mul (b i) (c i)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat nat_join O l (fun i : nat => @msum nat nat_join O i (fun j : nat => mul (add (mul (b i) (c j)) (mul (b j) (c i))) (@mscal nat mul (S O) (add (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (S j) (S (S O)))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) (nat_join (@msum nat nat_join O l (fun i : nat => mul (mul (b i) (c i)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat nat_join O l (fun i : nat => @msum nat nat_join O i (fun j : nat => mul (add (mul (b i) (c j)) (mul (b j) (c i))) (@mscal nat mul (S O) (add (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (S j) (S (S O)))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) *)
      apply nat_ortho_plus_join.
(* Goal: @eq nat (nat_meet (@msum nat nat_join O l (fun i : nat => mul (mul (b i) (c i)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat nat_join O l (fun i : nat => @msum nat nat_join O i (fun j : nat => mul (add (mul (b i) (c j)) (mul (b j) (c i))) (@mscal nat mul (S O) (add (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (S j) (S (S O)))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) O *)
      apply nat_ortho_joins.
(* Goal: forall (i j : nat) (_ : lt i l) (_ : lt j l), @eq nat (nat_meet (mul (mul (b i) (c i)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))) (@msum nat nat_join O j (fun j0 : nat => mul (add (mul (b j) (c j0)) (mul (b j0) (c j))) (@mscal nat mul (S O) (add (@mscal nat mul (S O) (S j) (S (S O))) (@mscal nat mul (S O) (S j0) (S (S O)))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) O *)
      intros i j Hi Hj; apply nat_ortho_joins_left.
(* Goal: forall (i0 : nat) (_ : lt i0 j), @eq nat (nat_meet (mul (mul (b i) (c i)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))) (mul (add (mul (b j) (c i0)) (mul (b i0) (c j))) (@mscal nat mul (S O) (add (@mscal nat mul (S O) (S j) (S (S O))) (@mscal nat mul (S O) (S i0) (S (S O)))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) O *)
      intros k Hk.
      apply nat_meet_powers_neq with (q := 4*q); auto; try omega.
      * apply power_2_n_ij_neq; omega.
      * apply Hbc_2; omega.
    Qed.

    Let Hr_1 : (r-1)*u1 = ∑ l (fun i => (r-1)*power (power (S (S i)) 2) r).
    Proof. rewrite sum_0n_scal_l; auto. Qed.

    Let Hr_2 : (r-1)*u1 = msum nat_join 0 l (fun i => (r-1)*power (power (S (S i)) 2) r).
    Proof.
(* Goal: @eq nat (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat nat_join O l (fun i : nat => mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) *)
      destruct Hb as (H1 & Hb1 & Hb2).
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      destruct Hc as (_ & Hc1 & Hc2).
(* Goal: @eq nat (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat nat_join O l (fun i : nat => mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) *)
      rewrite Hr_1.
      apply sum_powers_ortho with (q := 4*q); auto; try omega.
      + intros; omega.
      + intros ? ? ? ? E; apply power_2_inj in E; omega.
    Qed.
   
    Fact cipher_mult_eq : (cb*cc)⇣((r-1)*u1) = ∑ l (fun i => (b i*c i)*power (power (S (S i)) 2) r).
    Proof.
(* Goal: @eq nat (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat nat_join O l (fun i : nat => mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) *)
      destruct Hb as (H1 & Hb1 & Hb2).
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      destruct Hc as (_ & Hc1 & Hc2).
      rewrite eq2, Hbc_3, Hr_2.
      rewrite nat_meet_comm, nat_meet_join_distr_l.
      rewrite <- Hr_2 at 1; rewrite Hr_1, <- Hbc_3.
      rewrite meet_sum_powers with (q := 4*q); auto; try (intros; omega).
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
      2: intros; apply power_smono_l; omega.
      rewrite (proj2 (nat_ortho_joins _ _ _ _)), nat_join_n0.
      * apply msum_ext; intros i Hi; f_equal.
        rewrite nat_meet_comm; apply binary_le_nat_meet, power_2_minus_1_gt; auto.
      * intros i j Hi Hj.
        apply nat_ortho_joins_left.
        intros k Hk; apply nat_meet_powers_neq with (q := 4*q); auto; try omega.
        + apply power_2_n_ij_neq; omega.
        + apply Hbc_2; omega.
    Qed.

  End mult_utils.
  
  Section mult.

    Variable (a b c : nat-> nat) (ca cb cc : nat) 
             (Ha : is_cipher_of a ca)
             (Hb : is_cipher_of b cb) 
             (Hc : is_cipher_of c cc).

    Definition Code_mult := 
                l = 0 
             \/ l <> 0 
             /\ exists v v1 r' r'' p, 
                        r'' = r 
                     /\ r'' = r'+1 
                     /\ seqs_of_ones v v1 
                     /\ p = (ca*v)⇣(r'*v1) 
                     /\ p = (cb*cc)⇣(r'*v1).

    Lemma Code_mult_spec : Code_mult <-> forall i, i < l -> a i = b i * c i. 
    Proof.
(* Goal: iff Code_mult (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) *)
      unfold Code_mult; symmetry.
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      destruct Ha as (Hlq & Ha1 & Ha2).
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      destruct Hb as (_ & Hb1 & Hb2).
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      destruct Hc as (_ & Hc1 & Hc2).
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      destruct (eq_nat_dec l 0) as [ | Hl ].
      + subst l; split; intros; auto; omega.
      + split.
        * intros H; right; split; try omega.
          exists u, u1, (r-1), r, (ca * u ⇣ ((r-1) * u1)).
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          split; auto; split; try omega.
(* Goal: and (seqs_of_ones (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (and (@eq nat (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) (@eq nat (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (nat_meet (mul cb cc) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))))) *)
          repeat (split; auto).
(* Goal: forall (_ : @eq nat (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul r' (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (nat_meet (mul cb cc) (mul r' (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
          generalize (is_cipher_of_u Hlq); intros H2.
(* Goal: forall (_ : @eq nat (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (nat_meet (mul cb cc) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
          rewrite cipher_mult_eq with (1 := Ha) (2 := H2).
(* Goal: forall (_ : @eq nat (@msum nat add O l (fun i : nat => mul (mul (a i) (S O)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (nat_meet (mul cb cc) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
          rewrite cipher_mult_eq with (1 := Hb) (2 := Hc).
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          apply msum_ext; intros; rewrite H; try ring; omega.
        * intros [ | (_ & v & v1 & r' & r'' & p & H0 & H1 & H2 & H3 & H4) ]; try (destruct Hl; auto; fail).
(* Goal: forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
          destruct H2 as (_ & ? & ?); subst v v1.
(* Goal: forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
          rewrite H3 in H4.
(* Goal: forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
          revert H4.
(* Goal: forall (_ : @eq nat (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul r' (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (nat_meet (mul cb cc) (mul r' (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
          generalize (is_cipher_of_u Hlq); intros H2.
          replace r' with (r-1) by omega.
(* Goal: forall (_ : @eq nat (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (nat_meet (mul cb cc) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
          rewrite cipher_mult_eq with (1 := Ha) (2 := H2).
(* Goal: forall (_ : @eq nat (@msum nat add O l (fun i : nat => mul (mul (a i) (S O)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (nat_meet (mul cb cc) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
          rewrite cipher_mult_eq with (1 := Hb) (2 := Hc).
(* Goal: forall (_ : @eq nat (@msum nat add O l (fun i : nat => mul (mul (a i) (S O)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (@msum nat add O l (fun i : nat => mul (mul (b i) (c i)) (@mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
          intros E.
(* Goal: forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i)) *)
          intros i Hi. 
          rewrite <- power_decomp_unique with (5 := E); auto; try omega.
          - intros; apply power_smono_l; omega.
          - intros j Hj; rewrite Nat.mul_1_r.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
            apply lt_le_trans with (1 := Ha1 _ Hj), power_mono_l; omega.
          - intros; apply mult_lt_power_2_4; auto.
    Qed.

  End mult.

  Section inc_seq.

    Definition CodeNat c := is_cipher_of (fun i => i) c.

    Let IncSeq_dio_priv y : CodeNat y <-> l = 0 /\ 1 < q /\ y = 0 
                                  \/ 0 < l 
                                  /\ exists z v v1, 
                                        seqs_of_ones v v1 
                                     /\ Code y
                                     /\ Code z
                                     /\ y + l*(power (power (S l) 2) r) = (z*v)⇣((r-1) * v1)
                                     /\ y+v1+power (power 1 2) r = z + power (power (S l) 2) r.
    Proof.
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
      split.
      + intros (H1 & H2 & H3).
        destruct (le_lt_dec l 0) as [ | Hl ].
        - assert (l = 0) by omega; subst l.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          rewrite msum_0 in H3; left; omega.
        - right; split; auto.
          exists (∑ l (fun i => (S i) * power (power (S i) 2) r)), u, u1; split; auto.
(* Goal: is_digit (@msum nat add O (S n) (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) p (f i) (a i) *)
          { split; auto. }
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
          split.
(* Goal: is_digit (@msum nat add O (S n) (fun i : nat => mul (a i) (@mscal nat mul (S O) (f i) p))) p (f i) (a i) *)
          { rewrite H3; exists (fun i => i); split; auto. }
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
          split.
(* Goal: lt (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) q (S (S O))) *)
(* Goal: lt (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) (mul (@mscal nat mul (S O) q (S (S O))) (@mscal nat mul (S O) q (S (S O)))) *)
          { exists S; repeat (split; auto).
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
            intros; apply lt_le_trans with q; try omega.
            apply power_ge_n; auto. }
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
          split.
(* Goal: lt (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) q (S (S O))) *)
(* Goal: lt (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) (mul (@mscal nat mul (S O) q (S (S O))) (@mscal nat mul (S O) q (S (S O)))) *)
          { rewrite cipher_mult_eq with (b := S) (c := fun _ => 1).
            * rewrite H3.
              rewrite <- msum_plus1 with (f := fun i => i*power (power (S i) 2) r); auto.
              rewrite msum_S, Nat.mul_0_l, Nat.add_0_l.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
              apply msum_ext; intros; ring.
            * repeat split; auto; intros.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
              apply lt_le_trans with q; try omega.
              apply power_ge_n; auto.
            * apply is_cipher_of_u; auto. }
(* Goal: lt (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) q (S (S O))) *)
(* Goal: lt (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) (mul (@mscal nat mul (S O) q (S (S O))) (@mscal nat mul (S O) q (S (S O)))) *)
          { rewrite H3.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
            destruct l as [ | l' ]; try omega.
            rewrite msum_S, Nat.mul_0_l, Nat.add_0_l.
(* Goal: @eq nat (add (S O) (mul (sub r (S O)) (@msum nat add O (S l) (fun i : nat => @mscal nat mul (S O) i r)))) (@mscal nat mul (S O) (S l) r) *)
            rewrite msum_plus1; auto.
            rewrite plus_assoc.
(* Goal: forall _ : @eq nat O (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (g i) r)), and (@eq nat O (S m)) (forall (i : nat) (_ : lt i O), @eq nat (f i) (g i)) *)
            rewrite msum_S.
            rewrite <- msum_sum; auto.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
            2: intros; ring.
            rewrite Nat.mul_1_l, plus_comm.
            repeat rewrite <- plus_assoc; do 2 f_equal.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
            apply msum_ext; intros; ring. }
      + intros [ (H1 & H2 & H3) | (Hl & z & v & v1 & H1 & H2 & H3 & H4 & H5) ].
        - split; subst; auto; split; intros; try omega.
          rewrite msum_0; auto.
        - destruct H1 as (Hq & ? & ?); subst v v1.
(* Goal: iff (forall (i : nat) (_ : lt i l), @eq nat (a i) (mul (b i) (c i))) (or (@eq nat l O) (and (not (@eq nat l O)) (@ex nat (fun v : nat => @ex nat (fun v1 : nat => @ex nat (fun r' : nat => @ex nat (fun r'' : nat => @ex nat (fun p : nat => and (@eq nat r'' (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))) (and (@eq nat r'' (add r' (S O))) (and (seqs_of_ones v v1) (and (@eq nat p (nat_meet (mul ca v) (mul r' v1))) (@eq nat p (nat_meet (mul cb cc) (mul r' v1)))))))))))))) *)
          split; auto; split.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          { intros i Hi; apply lt_le_trans with q; try omega.
            apply power_ge_n; auto. }
          destruct H2 as (f & Hf).
          destruct H3 as (g & Hg).
          generalize (is_cipher_of_u Hq); intros Hu.
          rewrite cipher_mult_eq with (1 := Hg) (2 := Hu) in H4.
          destruct Hf as (_ & Hf & Hy).
          destruct Hg as (_ & Hg & Hz).
          set (h i := if le_lt_dec l i then l else f i).
          assert (y+l*power (power (S l) 2) r = ∑ (S l) (fun i => h i * power (power (S i) 2) r)) as H6.
(* Goal: lt (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) q (S (S O))) *)
(* Goal: lt (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) (mul (@mscal nat mul (S O) q (S (S O))) (@mscal nat mul (S O) q (S (S O)))) *)
          { rewrite msum_plus1; auto; f_equal.
            * rewrite Hy; apply msum_ext.
              intros i Hi; unfold h.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
              destruct (le_lt_dec l i); try omega.
            * unfold h.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
              destruct (le_lt_dec l l); try omega. }
          rewrite H4 in H6.
          set (g' i := match i with 0 => 0 | S i => g i end).
          assert ( ∑ (S l) (fun i => g' i * power (power (S i) 2) r)
                 = ∑ l (fun i : nat => g i * 1 * power (power (S (S i)) 2) r)) as H7.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
          { unfold g'; rewrite msum_S; apply msum_ext; intros; ring. }
          rewrite <- H7 in H6.
          assert (forall i, i < S l -> g' i = h i) as H8.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          { apply power_decomp_unique with (5 := H6); try omega. 
            * intros; apply power_smono_l; omega. 
            * unfold g'; intros [ | i ] Hi; try omega.
              apply lt_S_n in Hi.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
              apply lt_le_trans with (1 := Hg _ Hi), power_mono_l; omega.
            * intros i Hi; unfold h.
              destruct (le_lt_dec l i) as [ | Hi' ].
              + apply lt_le_trans with (4*q); try omega.
                apply power_ge_n; auto.
              + apply lt_le_trans with (1 := Hf _ Hi'), power_mono_l; omega.  }
          assert (h 0 = 0) as E0.
          { rewrite <- H8; simpl; omega. }
          assert (forall i, i < l -> h (S i) = g i) as E1.
          { intros i Hi; rewrite <- H8; simpl; omega. }
          assert (f 0 = 0) as E3.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          { unfold h in E0; destruct (le_lt_dec l 0); auto; omega. }
          assert (forall i, S i < l -> f (S i) = g i) as E4.
(* Goal: lt (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) q (S (S O))) *)
(* Goal: lt (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) (mul (@mscal nat mul (S O) q (S (S O))) (@mscal nat mul (S O) q (S (S O)))) *)
          { intros i Hi; specialize (E1 i); unfold h in E1.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
            destruct (le_lt_dec l (S i)); omega. }
          assert (g (l-1) = l) as E5.
          { specialize (E1 (l-1)); unfold h in E1.
            destruct (le_lt_dec l (S (l-1))); omega. }  
          clear H6 H7 g' H8 E0 E1 h H4.
          assert (y + u1 + power (power 1 2) r = 
                  ∑ l (fun i => (1+f i) * power (power (S i) 2) r)
                + power (power (S l) 2) r) as E1.
(* Goal: lt (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) q (S (S O))) *)
(* Goal: lt (mul (S (S O)) (@mscal nat mul (S O) q (S (S O)))) (mul (@mscal nat mul (S O) q (S (S O))) (@mscal nat mul (S O) q (S (S O)))) *)
          { rewrite sum_0n_distr_in_out.
            rewrite <- Hy, sum_0n_scal_l, Nat.mul_1_l.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
            destruct l as [ | l' ]; try omega.
(* Goal: @eq nat (add (S O) (mul (sub r (S O)) (@msum nat add O (S l) (fun i : nat => @mscal nat mul (S O) i r)))) (@mscal nat mul (S O) (S l) r) *)
            rewrite msum_plus1; auto.
(* Goal: @eq nat (add x x) (mul (S (S O)) x) *)
            rewrite msum_S; ring. }
          assert (forall i, i < l -> 1+f i = g i) as E2.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          { apply power_decomp_unique with (f := fun i => power (S i) 2) (p := r); try omega.
            + intros; apply power_smono_l; omega.
            + intros i Hi; apply le_lt_trans with (power q 2); auto.
              * apply Hf; auto.
              * apply power_smono_l; omega. 
            + intros i Hi; apply lt_le_trans with (1 := Hg _ Hi), power_mono_l; omega. } 
(* Goal: @eq nat (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (k i) r)) (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) r)) *)
          rewrite Hy; apply msum_ext.
          clear Hy Hf Hg Hz H5 E5 E1 Hu.
          intros i Hi; f_equal; revert i Hi.
          induction i as [ | i IHi ]; intros Hi; auto.
          rewrite E4, <- E2; try omega.
(* Goal: @eq nat u (@msum nat add O (S m) (fun i : nat => @mscal nat mul (S O) (f1 i) r)) *)
          rewrite IHi; omega.
    Qed.

    Lemma CodeNat_dio y : CodeNat y <-> l = 0 /\ 1 < q /\ y = 0 
                                  \/ 0 < l 
                                  /\ exists z v v1 p0 p1 p2 r1,
                                        p0 = r
                                     /\ r1+1 = p0 
                                     /\ p1 = power (1+l) 2
                                     /\ p2 = power p1 p0 
                                     /\ seqs_of_ones v v1 
                                     /\ Code y
                                     /\ Code z
                                     /\ y + l*p2 = (z*v) ⇣ (r1 * v1)
                                     /\ y + v1 + p0*p0 = z + p2.
    Proof.
      rewrite IncSeq_dio_priv; split; (intros [ H | H ]; [ left | right ]); auto; revert H;
        intros (H1 & H); split; auto; clear H1; revert H.
      + intros (z & v & v1 & H1 & H2 & H3 & H4 & H5).
        exists z, v, v1, r, (power (S l) 2), (power (power (S l) 2) r), (r-1); repeat (split; auto).
        * destruct H1; omega.
        * rewrite <- H5; f_equal.
(* Goal: @eq nat (@mscal nat mul (S O) (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) (add q (add q (add q (add q O)))) (S (S O)))) (mul (@mscal nat mul (S O) (add q (add q (add q (add q O)))) (S (S O))) (@mscal nat mul (S O) (add q (add q (add q (add q O)))) (S (S O)))) *)
          rewrite power_1, power_S, power_1; auto.
      + intros (z & v & v1 & p0 & p1 & p2 & r1 & H1 & H2 & H3 & H4 & H5 & H6 & H7 & H8 & H9).
        assert (r1 = r - 1) by omega; clear H2; subst.
(* Goal: and (seqs_of_ones (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (and (@eq nat (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))))) (@eq nat (nat_meet (mul ca (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S i) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O)))))) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))) (nat_meet (mul cb cc) (mul (sub (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))) (S O)) (@msum nat add O l (fun i : nat => @mscal nat mul (S O) (@mscal nat mul (S O) (S (S i)) (S (S O))) (@mscal nat mul (S O) (mul (S (S (S (S O)))) q) (S (S O))))))))) *)
        exists z, v, v1; repeat (split; auto).
        simpl in H9 |- *; rewrite <- H9; f_equal.
(* Goal: @eq nat (@mscal nat mul (S O) (@mscal nat mul (S O) (S O) (S (S O))) (@mscal nat mul (S O) (add q (add q (add q (add q O)))) (S (S O)))) (mul (@mscal nat mul (S O) (add q (add q (add q (add q O)))) (S (S O))) (@mscal nat mul (S O) (add q (add q (add q (add q O)))) (S (S O)))) *)
        rewrite power_1, power_S, power_1; auto.
    Qed.
      
  End inc_seq.

End sums.  

Check Code_plus_spec.
Check Code_mult_spec.
Check CodeNat_dio.
