Require Import Arith Lia List Bool.

From Undecidability.Shared.Libs.DLW.Utils
  Require Import utils_tac gcd sums rel_iter bool_nat power_decomp prime.

Set Implicit Arguments.

Set Default Proof Using "Type".

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).

#[export] Hint Resolve power2_gt_0 : core.

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.
    intros .
    replace (2*k) with (k+k) by .
    rewrite power_plus.
    apply lt_le_trans with ((S u)*S v).
    simpl; rewrite (mult_comm _ (S _)); simpl; rewrite mult_comm; .
    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.
    intros .
    apply lt_le_trans with (1 := mult_lt_power_2 _ ).
    apply power_mono_l; .
  Qed.

  Fact mult_lt_power_2_4' u1 v1 u2 v2 k :
                < power k 2
             < power k 2
             < power k 2
             < power k 2
             *+* < power (4*k) 2.
  Proof.
    intros .
    destruct (eq_nat_dec k 0) as [ ? | Hk ].
    - subst k; simpl.
      rewrite power_0 in *.
      destruct ; destruct ; destruct ; destruct ; subst; .
    - apply lt_le_trans with (power (S (2*k)) 2).
      + rewrite power_S, mult_2_eq_plus.
        apply plus_lt_compat; apply mult_lt_power_2; auto.
      + apply power_mono_l; .
  Qed.

End stability_of_power.

Section power_decomp.

  Variable (p : ) (Hp : 2 p).

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

  Fact power_decomp_lt n f a q :
           ( i j, i < j < n f i < f j)
         ( i, i < n f i < q)
         ( i, i < n a i < p)
         ∑ n ( i a i * power (f i) p) < power q p.
  Proof using Hp.
    revert q; induction n as [ | n IHn ]; intros q Ha.
    + rewrite msum_0; apply power_ge_1; .
    + 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.
        rewrite Nat.mul_1_l.
        apply IHn.
        - intros; apply ; .
        - intros; apply ; .
        - intros; apply Ha; .
      * rewrite Nat.mul_add_distr_r.
        replace q with (S (q-1)).
        - rewrite power_S; apply mult_le_compat; auto.
          ++ apply Ha; auto.
          ++ apply power_mono_l; try .
             generalize ( n); intros; .
        - generalize ( 0); intros; .
  Qed.

  Lemma power_decomp_is_digit n a f :
           ( i j, i < j < n f i < f j)
         ( i, i < n a i < p)
         i, i < n is_digit (∑ n ( i a i * power (f i) p)) p (f i) (a i).
  Proof using Hp.
    intros Hf Ha.
    induction n as [ | n IHn ]; intros i Hi.
    + .
    + split; auto.
      exists (∑ (n-i) ( j a (S i + j) * power (f (S i+j) - f i - 1) p)),
             (∑ i ( j a j * power (f j) p)); split.
      - replace (S n) with (S i + (n-i)) by .
        rewrite msum_plus, msum_plus1; auto.
        rewrite plus_assoc, plus_comm; f_equal.
        rewrite Nat.mul_add_distr_r, plus_comm; f_equal.
        rewrite mult_assoc, mult_comm, sum_0n_scal_l.
        apply msum_ext.
        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; .
      - apply power_decomp_lt; auto.
        * intros; apply Hf; .
        * intros; apply Ha; .
  Qed.

  Theorem power_decomp_unique n f a b :
            ( i j, i < j < n f i < f j)
          ( i, i < n a i < p)
          ( i, i < n b i < p)
          ∑ n ( i a i * power (f i) p)
          = ∑ n ( i b i * power (f i) p)
          i, i < n a i = b i.
  Proof using Hp.
    intros Hf Ha Hb E i Hi.
    generalize (power_decomp_is_digit _ _ Hf Ha Hi)
               (power_decomp_is_digit _ _ Hf Hb Hi).
    rewrite E; apply is_digit_fun.
  Qed.

End power_decomp.

Section power_decomp_uniq.

  Variable (p : ) (Hp : 2 p).

  Theorem power_decomp_factor n f a :
           ( i, 0 < i < S n f 0 < f i)
         ∑ (S n) ( i a i * power (f i) p)
         = ∑ n ( i a (S i) * power (f (S i) - f 0 - 1) p) * power (S (f 0)) p
         + a 0 * power (f 0) p.
  Proof using Hp.
    intros Hf.
    rewrite msum_S, plus_comm; f_equal.
    rewrite sum_0n_scal_r.
    apply msum_ext.
    intros i Hi.
    rewrite mult_assoc; f_equal.
    rewrite power_plus; f_equal.
    generalize (Hf (S i)); intros; .
  Qed.

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

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


  Theorem power_decomp_unique' n f a b :
            ( i j, i < j < n f i < f j)
          ( i, i < n a i < p)
          ( i, i < n b i < p)
          ∑ n ( i a i * power (f i) p)
          = ∑ n ( i b i * power (f i) p)
          i, i < n a i = b i.
  Proof using Hp.
    revert f a b.
    induction n as [ | n IHn ]; intros f a b Hf Ha Hb.
    + intros; .
    + assert ( i, 0 < i < S n f 0 < f i)
        by (intros; apply Hf; ).
      do 2 (rewrite power_decomp_factor; auto).
      intros E.
      apply div_rem_uniq in E; auto.
      * destruct E as ( & ).
        intros [ | i ] Hi.
        - revert ; rewrite Nat.mul_cancel_r; auto.
        - apply IHn with (4 := ); try .
          ++ intros u j Hu; apply lt_minus_cancel; split; apply Hf; .
          ++ intros; apply Ha; .
          ++ intros; apply Hb; .
      * rewrite power_S.
        apply Nat.mul_lt_mono_pos_r.
        - apply power_ge_1; .
        - apply Ha; .
      * rewrite power_S.
        apply Nat.mul_lt_mono_pos_r.
        - apply power_ge_1; .
        - apply Hb; .
  Qed.

End power_decomp_uniq.

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

Section power_injective.

  Local Lemma power_2_inj_1 i j n : j < i 2* power n 2 power i 2 + power j 2.
  Proof.
    rewrite power_S; intros E.
     generalize (@power_ge_1 j 2); intro C.
     destruct (lt_eq_lt_dec i (S n)) as [ [ | ] | ].
     + apply power_mono_l with (x := 2) in ; auto.
       rewrite power_S in .
       apply power_mono_l with (x := 2) in ; auto.
       rewrite power_S in ; .
     + subst i; .
     + apply power_mono_l with (x := 2) in ; auto.
      rewrite power_S in ; .
  Qed.

  Fact power_2_n_ij_neq i j n : i j power (S n) 2 power i 2 + power j 2.
  Proof.
    intros H.
    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.
    intros H.
    destruct (lt_eq_lt_dec i j) as [ [ C | C ] | C ]; auto;
      apply power_smono_l with (x := 2) in C; .
  Qed.

  Local Lemma power_plus_lt a b c : a < b < c power a 2 + power b 2 < power c 2.
  Proof.
    intros [ ].
    apply power_mono_l with (x := 2) in ; auto.
    apply power_smono_l with (x := 2) in ; auto.
    rewrite power_S in ; .
  Qed.

  Local Lemma power_inj_2 i1 j1 i2 j2 :
              <
           <
           power 2 + power 2 = power 2 + power 2
           = = .
  Proof.
    intros .
    destruct (lt_eq_lt_dec ) as [ [ C | C ] | C ].
    + generalize (@power_plus_lt ); intros; .
    + split; auto; apply power_2_inj; subst; .
    + generalize (@power_plus_lt ); intros; .
  Qed.

  Theorem sum_2_power_2_injective i1 j1 i2 j2 :
              
           
            power 2 + power 2 = power 2 + power 2
            = = .
  Proof.
    intros E.
    destruct (eq_nat_dec ) as [ | ];
    destruct (eq_nat_dec ) as [ | ].
    + subst .
      assert ( = ); auto.
      do 2 rewrite mult_2_eq_plus, power_S in E.
      apply power_2_inj in E; .
    + subst ; rewrite mult_2_eq_plus in E.
      apply power_2_inj_1 in E; .
    + subst ; symmetry in E.
      rewrite mult_2_eq_plus in E.
      apply power_2_inj_1 in E; .
    + revert E; apply power_inj_2; .
  Qed.

End power_injective.

Fact divides_power p a b : a b divides (power a p) (power b p).
Proof.
  * induction 1 as [ | b H IH ].
    + apply divides_refl.
    + apply divides_trans with (1 := IH).
      rewrite power_S; apply divides_mult, divides_refl.
Qed.

Fact divides_msum k n f : ( i, i < n divides k (f i)) divides k (∑ n f).
Proof.
  revert f; induction n as [ | n IHn ]; intros f Hf.
  + rewrite msum_0; apply divides_0.
  + rewrite msum_S; apply divides_plus.
    * apply Hf; .
    * apply IHn; intros; apply Hf; .
Qed.

Fact inc_seq_split_lt n f k :
         ( i j, i < j < n f i < f j)
       { p | p n ( i, i < p f i < k) i, p i < n k f i }.
Proof.
  revert f; induction n as [ | n IHn ]; intros f Hf.
  + exists 0; split; auto; split; intros; .
  + destruct (le_lt_dec k (f 0)) as [ H | H ].
    - exists 0; split; try .
      split; intros i Hi; try .
      destruct i as [ | i ]; auto.
      apply le_trans with (1 := H), lt_le_weak, Hf; .
    - destruct (IHn ( i f (S i))) as (p & & & ).
      * intros; apply Hf; .
      * exists (S p); split; try ; split.
        ++ intros [ | i ] Hi; auto; apply ; .
        ++ intros [ | i ] Hi; try ; apply ; .
Qed.

Fact inc_seq_split_le n f h : ( i j, i < j < n f i < f j)
                    { q | q n
                          ( i, i < q f i h)
                          ( i, q i < n h < f i) }.
Proof.
  intros Hf.
  destruct inc_seq_split_lt with (1 := Hf) (k := S h)
    as (q & & & ); exists q; split; auto; split.
  + intros i Hi; specialize ( _ Hi); .
  + intros i Hi; specialize ( _ Hi); .
Qed.

Fact divides_lt p q : q < p divides p q q = 0.
Proof.
  intros ([ | k] & ); auto.
  revert ; simpl; generalize (k *p); intros; .
Qed.

Fact sum_powers_inc_lt_last n f r :
        2 r
      ( i j, i < j n f i < f j)
      ∑ (S n) ( i power (f i) r) < power (S (f n)) r.
Proof.
  intros Hr.
  revert f.
  induction n as [ | n IHn ]; intros f Hf.
  + rewrite msum_1; auto; apply power_smono_l; auto.
  + rewrite msum_plus1; auto.
    rewrite power_S.
    apply lt_le_trans with (power (S (f n)) r + power (f (S n)) r).
    * apply plus_lt_compat_r; auto.
      apply IHn; intros; apply Hf; .
    * assert (power (S (f n)) r power (f (S n)) r) as H.
      { apply power_mono_l; try ; apply Hf; . }
      apply le_trans with (2 * power (f (S n)) r); try .
      apply mult_le_compat; auto.
Qed.

Fact sum_powers_inc_lt n f p r :
        2 r
      ( i, i < n f i < p)
      ( i j, i < j < n f i < f j)
      ∑ n ( i power (f i) r) < power p r.
Proof.
  destruct n as [ | n ].
  + intros H _ _; rewrite msum_0; apply power_ge_1; .
  + intros .
    apply lt_le_trans with (power (S (f n)) r).
    * apply sum_powers_inc_lt_last; auto.
      intros; apply ; .
    * apply power_mono_l; try .
      apply ; auto.
Qed.


Fact sum_powers_injective r n f m g :
       2 r
     ( i j, i < j < n f i < f j)
     ( i j, i < j < m g i < g j)
     ∑ n ( i power (f i) r) = ∑ m ( i power (g i) r)
     n = m i, i < n f i = g i.
Proof.
  intros Hr; revert m f g.
  induction n as [ | n IHn ]; intros m f g Hf Hg.
  + rewrite msum_0.
    destruct m as [ | m ].
    * rewrite msum_0; split; auto; intros; .
    * rewrite msum_S.
      generalize (@power_ge_1 (g 0) r); intros; exfalso; .
  + destruct m as [ | m ].
    * rewrite msum_0, msum_S; intros; exfalso.
       generalize (@power_ge_1 (f 0) r); intros; exfalso; .
    * destruct (lt_eq_lt_dec (f n) (g m)) as [ [E|E]| E].
      - rewrite msum_plus1 with (n := m); auto.
        intros; exfalso.
        assert (∑ (S n) ( i power (f i) r) < power (g m) r) as C; try .
        apply sum_powers_inc_lt; auto.
        intros i Hi.
        destruct (eq_nat_dec i n); subst; auto.
        apply lt_trans with (2 := E), Hf; .
      - do 2 (rewrite msum_plus1; auto); intros C.
        destruct (IHn m f g) as ( & ).
        ++ intros; apply Hf; .
        ++ intros; apply Hg; .
        ++ rewrite E in C; .
        ++ split; subst; auto.
           intros i Hi.
           destruct (eq_nat_dec i m); subst; auto.
           apply ; .
      - rewrite msum_plus1 with (n := n); auto.
        intros; exfalso.
        assert (∑ (S m) ( i power (g i) r) < power (f n) r) as C; try .
        apply sum_powers_inc_lt; auto.
        intros i Hi.
        destruct (eq_nat_dec i m); subst; auto.
        apply lt_trans with (2 := E), Hg; .
Qed.

Fact power_divides_sum_power r p n f :
         2 r
       0 < n
       ( i j, i < j < n f i < f j)
       divides (power p r) (∑ n ( i power (f i) r)) p f 0.
Proof.
  intros Hr Hn Hf.
  split.
  + destruct inc_seq_split_lt with (k := p) (1 := Hf) as (k & & & ).
    replace n with (k+(n-k)) by .
    rewrite msum_plus; auto.
    rewrite plus_comm; intros H.
    apply divides_plus_inv in H.
    2: apply divides_msum; intros; apply divides_power, ; .
    destruct k as [ | k ].
    * apply ; .
    * apply divides_lt in H.
      - rewrite msum_S in H.
        generalize (@power_ge_1 (f 0) r); intros; .
      - apply sum_powers_inc_lt; auto.
        intros; apply Hf; .
  + intros H.
    apply divides_msum.
    intros i Hi; apply divides_power.
    apply le_trans with (1 := H).
    destruct i; auto.
    generalize (Hf 0 (S i)); intros; .
Qed.

Fact smono_upto_injective n f :
       ( i j, i < j < n f i < f j)
     ( i j, i < n j < n f i = f j i = j).
Proof.
  intros Hf i j Hi Hj E.
  destruct (lt_eq_lt_dec i j) as [ [H|] | H ]; auto.
  + generalize (@Hf i j); intros; .
  + generalize (@Hf j i); intros; .
Qed.

Fact product_sums n f g : (∑ n f)*(∑ n g)
                         = ∑ n ( i f i*g i)
                         + ∑ n ( i ∑ i ( j f i*g j + f j*g i)).
Proof.
  induction n as [ | n IHn ].
  + repeat rewrite msum_0; auto.
  + repeat rewrite msum_plus1; auto.
    repeat rewrite Nat.mul_add_distr_l.
    repeat rewrite Nat.mul_add_distr_r.
    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 ( i f i*f i) + 2*∑ n ( i ∑ i ( j f i*f j)).
  Proof.
    rewrite product_sums, sum_0n_scal_l; f_equal.
    apply msum_ext; intros; rewrite sum_0n_scal_l.
    apply msum_ext; intros; ring.
  Qed.

  Fact sum_regroup r k n f :
          ( i, i < n f i < k)
        ( i j, i < j < n f i < f j)
        { g | ∑ n ( i power (f i) r)
              = ∑ k ( i g i * power i r)
              ( i, i < k g i 1)
              ( i, k i g i = 0) }.
  Proof.
    revert k f; induction n as [ | n IHn ]; intros k f .
    + exists ( _ 0); split; auto.
      rewrite msum_0, msum_of_unit; auto.
    + destruct (IHn (f n) f) as (g & & & ).
      * intros; apply ; .
      * intros; apply ; .
      * exists ( i if eq_nat_dec i (f n) then 1 else g i).
        split; [ | split ].
        - rewrite msum_plus1, ; auto.
          replace k with (f n + S (k - f n -1)).
          2: generalize ( n); intros; .
          rewrite msum_plus; auto; f_equal.
          ++ apply msum_ext.
             intros i He.
             destruct (eq_nat_dec i (f n)); try ring; .
          ++ rewrite msum_S, msum_of_unit; auto.
             ** repeat (rewrite plus_comm; simpl).
                destruct (eq_nat_dec (f n) (f n)); try ring; .
             ** intros i Hi.
                destruct (eq_nat_dec (f n+S i) (f n)); try .
                rewrite ; .
        - intros i Hi.
          destruct (eq_nat_dec i (f n)); auto.
          destruct (le_lt_dec (f n) i).
          ++ rewrite ; .
          ++ apply ; .
        - intros i Hi.
          generalize ( n); intros.
          destruct (eq_nat_dec i (f n)); try .
          apply ; .
  Qed.

  Section sum_sum_regroup.

    Variable (r n k : ) (f : )
             ( : i, i < n f i k)
             ( : i j, i < j < n f i < f j).

    Theorem sum_sum_regroup : { g | ∑ n ( i ∑ i ( j power (f i + f j) r))
                                  = ∑ (2*k) ( i g i * power i r)
                                   i, g i n }.
    Proof using .
      revert n f .
      induction n as [ | p IHp ]; intros f .
      + exists ( _ 0); split; auto.
        rewrite msum_0.
        simpl; rewrite msum_of_unit; auto.
      + destruct (IHp f) as (g & & ).
        * intros; apply ; .
        * intros; apply ; .
        * destruct sum_regroup with (r := r) (n := p) (f := j f p + f j) (k := 2*k)
            as ( & & & ).
          - intros i Hi; generalize (@ p) (@ i p); intros; .
          - intros i j H; generalize (@ i j); intros; .
          - assert ( i, i 1) as .
            { intro i; destruct (le_lt_dec (2*k) i); auto; rewrite ; . }
            exists ( i g i + i); split.
            ++ rewrite msum_plus1; auto.
               rewrite , , msum_sum; auto.
               2: intros; ring.
               apply msum_ext; intros; ring.
            ++ intros i.
               generalize ( i) ( i); intros; .
    Qed.

  End sum_sum_regroup.

  Section all_ones.

    Local Lemma equation_inj x y a b : 1 x 1+x*a = y 1+x*b = y a = b.
    Proof.
      intros .
      rewrite in ; clear y .
      rewrite (@Nat.mul_cancel_l _ _ x); .
    Qed.

    Variables (r : ) (Hr : 2 r).

    Fact all_ones_equation l : 1+(r-1)*∑ l ( i power i r) = power l r.
    Proof using Hr.
      induction l as [ | l IHl ].
      * rewrite msum_0, Nat.mul_0_r, power_0; auto.
      * rewrite msum_plus1; auto.
        rewrite Nat.mul_add_distr_l, power_S.
        replace r with (1+(r-1)) at 4 by .
        rewrite Nat.mul_add_distr_r.
        rewrite IHl at 2; ring.
    Qed.

    Fact all_ones_dio l w : w = ∑ l ( i power i r) 1+(r-1)*w = power l r.
    Proof using Hr.
      split.
      + intros; subst; apply all_ones_equation.
      + intros H.
        apply equation_inj with (2 := H).
        * .
        * apply all_ones_equation.
    Qed.

  End all_ones.

  Section const_1.

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

    Let Hq : 1 q. Proof. . Qed.
    Let Hq' : 0 < 4*q. Proof. . Qed.

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

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

    Section all_ones.

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

      Local Lemma Hw_0 : w = ∑ n ( i 1*power i r).
      Proof using Hw. rewrite Hw; apply msum_ext; intros; ring. Qed.

      Fact all_ones_joins : w = msum nat_join 0 n ( i 1*power i r).
      Proof using Hl Hlq Hw.
        rewrite Hw_0.
        apply sum_powers_ortho with (q := 4*q); auto; try .
      Qed.

      Local Lemma Hw_1 : 2*w = ∑ n ( i 2*power i r).
      Proof using Hw.
        rewrite Hw_0, sum_0n_scal_l.
        apply msum_ext; intros; ring.
      Qed.

      Fact all_ones_2_joins : 2*w = msum nat_join 0 n ( i 2*power i r).
      Proof using Hl Hlq Hw.
        rewrite Hw_1.
        apply sum_powers_ortho with (q := 4*q); auto; try .
      Qed.

    End all_ones.

    Section increase.

      Variable (m k k' u w : ) (f : )
               (Hm : 2*m < r)
               ( : i, i < m f i k)
               ( : i j, i < j < m f i < f j)
               (Hw : w = ∑ k' ( i power i r))
               (Hu : u = ∑ m ( i power (f i) r)).

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

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

      Fact const_u_square : u * u = + .
      Proof using Hl Hlq Hw Hu Hm.
        unfold , .
        rewrite Hu, square_sum; f_equal.
        + apply msum_ext; intros; rewrite power_plus; f_equal; .
        + rewrite sum_0n_scal_l; apply msum_ext; intros i Hi.
          rewrite sum_0n_scal_l; apply msum_ext; intros j Hj.
          rewrite power_plus; ring.
      Qed.

      Local Lemma Hu1_0 : = ∑ m ( i 1*power (2*f i) r).
      Proof. apply msum_ext; intros; ring. Qed.

      Local Lemma Hseq_u a : a m ∑ a ( i 1*power (2*f i) r) = msum nat_join 0 a ( i 1*power (2*f i) r).
      Proof using Hw Hl Hlq Hm Hu.
        intros Ha.
        apply sum_powers_ortho with (q := 4*q); auto; try .
        intros i j Hi Hj ?; apply ; .
      Qed.

      Local Lemma Hu1 : = msum nat_join 0 m ( i 1*power (2*f i) r).
      Proof using Hw Hl Hlq Hm Hu.
        rewrite Hu1_0; apply Hseq_u; auto.
      Qed.

      Local Lemma Hu2_0 : = 2 * ∑ m ( i ∑ i ( j power (f i + f j) r)).
      Proof.
        unfold ; rewrite sum_0n_scal_l; apply msum_ext.
        intros; rewrite sum_0n_scal_l; apply msum_ext; auto.
      Qed.


      Local Lemma g_full : { g | ∑ m ( i ∑ i ( j power (f i + f j) r))
                      = ∑ (2*k) ( i : g i * power i r)
                       i : , g i m }.
      Proof using . apply sum_sum_regroup; auto. Qed.

      Let g := proj1_sig g_full.
      Local Lemma Hg1 : = ∑ (2*k) ( i (2*g i) * power i r).
      Proof.
        rewrite Hu2_0, (proj1 (proj2_sig g_full)), sum_0n_scal_l.
        apply msum_ext; unfold g; intros; ring.
      Qed.

      Local Lemma Hg2 i : 2*g i 2*m.
      Proof. apply mult_le_compat; auto; apply (proj2_sig g_full). Qed.

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

      Let : = msum nat_join 0 (2*k) ( i (2*g i) * power i r).
      Proof.
        rewrite Hg1.
        apply sum_powers_ortho with (q := 4*q); auto; .
      Qed.

      Let Hu1_u2_1 : ⇣ = 0.
      Proof.
        rewrite Hu1, .
        apply nat_ortho_joins.
        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.
          rewrite nat_meet_mult_power2.
          rewrite nat_meet_12n; auto.
        + rewrite nat_meet_powers_neq with (q := 4*q); auto; .
      Qed.

      Let Hu1_u2 : u*u = ⇡ .
      Proof.
        rewrite const_u_square.
        apply nat_ortho_plus_join; auto.
      Qed.

      Let : w = msum nat_join 0 k' ( i 1*power i r).
      Proof. rewrite Hw; apply all_ones_joins; auto. Qed.

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

      Local Lemma Hu2_w : ⇣ w = 0.
      Proof using H2w_1 Hu1_u2.
        rewrite , .
        destruct (le_lt_dec k' (2*k)) as [ Hk | Hk ].
        2: { apply nat_ortho_joins.
             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.
               rewrite nat_meet_12n; auto.
             + apply nat_meet_powers_neq with (q := 4*q); auto; try . }
        replace (2*k) with (k'+(2*k-k')) by .
        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.
        2: { intros i j .
             apply nat_meet_powers_neq with (q := 4*q); auto; try . }
        apply nat_ortho_joins.
        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.
          rewrite nat_meet_12n; auto.
        + apply nat_meet_powers_neq with (q := 4*q); auto; try .
      Qed.

      Fact const_u1_prefix : { q | q m u*u ⇣ w = ∑ q ( i 1*power (2*f i) r) }.
      Proof using H2w_1 Hu1_u2.
        destruct inc_seq_split_lt with (n := m) (f := i 2*f i) (k := k') as (a & & & ).
        + intros i j Hij; apply in Hij; .
        + exists a; split; auto.
          rewrite Hu1_u2, nat_meet_comm, nat_meet_join_distr_l.
          do 2 rewrite (nat_meet_comm w).
          rewrite Hu2_w, nat_join_n0.
          rewrite Hu1, .
          replace m with (a+(m-a)) by .
          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.
            apply binary_le_nat_meet.
            apply nat_joins_binary_le.
            intros i Hi.
            exists (2*f i); split; auto.
          * intros; apply nat_meet_powers_neq with (q := 4*q); auto; try .
            generalize ( (a + j)); intros; .
      Qed.

      Hypothesis (Hk : 2*k < k').

      Let Hu1_w : ⇣ w = .
      Proof.
        apply binary_le_nat_meet.
        rewrite Hu1, .
        apply nat_joins_binary_le.
        intros i Hi.
        exists (2*f i); split; auto.
        apply le_lt_trans with (2 := Hk), mult_le_compat; auto.
      Qed.

      Let Hu1_2w : ⇣ (2*w) = 0.
      Proof.
        rewrite H2w_1, Hu1, nat_ortho_joins.
        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 .
          rewrite nat_meet_12; auto.
        + apply nat_meet_powers_neq with (q := 4*q); auto; try .
      Qed.

      Fact const_u1_meet p : p = (u*u) ⇣ w p = .
      Proof using Hu1_w.
        rewrite Hu1_u2, nat_meet_comm, nat_meet_join_distr_l.
        do 2 rewrite (nat_meet_comm w).
        rewrite Hu1_w, Hu2_w, nat_join_n0; tauto.
      Qed.

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

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

      Let Hu2_1 : = msum nat_join 0 m ( i msum nat_join 0 i ( j 2*power (f i + f j) r)).
      Proof.
        unfold .
        apply double_sum_powers_ortho with (q := 4*q); auto; try .
        intros ? ? ? ? ? ?; repeat rewrite Hf; try .
        intros E.
        apply sum_2_power_2_injective in E; .
      Qed.


      Let Hu2_2w : ⇣ (2*w) = .
      Proof.
        apply binary_le_nat_meet.
        rewrite H2w_1, Hu2_1.
        apply nat_double_joins_binary_le.
        intros i j Hij.
        exists (f i + f j); split; auto.
        apply le_lt_trans with (2*f i); auto.
        + apply in Hij; .
        + apply le_lt_trans with (2 := Hk), mult_le_compat; auto.
          apply ; .
      Qed.

      Fact const_u2_meet p : p = (u*u) ⇣ (2*w) p = .
      Proof using Hu1_w Hu2_2w.
        rewrite Hu1_u2, nat_meet_comm, nat_meet_join_distr_l.
        do 2 rewrite (nat_meet_comm (2*w)).
        rewrite Hu1_2w, Hu2_2w, nat_join_0n; tauto.
      Qed.

    End increase.

    Let Hl'' : 2*l < r.
    Proof.
      unfold r.
      rewrite (mult_comm _ q), power_mult.
      change (power 4 2) with 16.
      apply power_smono_l with (x := 16) in Hlq; try .
      apply le_lt_trans with (2 := Hlq).
      rewrite plus_comm; simpl plus; rewrite power_S.
      apply mult_le_compat; try .
      apply power_ge_n; .
    Qed.

    Section const_1_cn.


      Variable (u : ) (Hu : u = ∑ l ( i power (power (S i) 2) r))
                            ( : = ∑ l ( i power (power (S (S i)) 2) r)).

      Let w := ∑ (S (power (S l) 2)) ( i power i r).
      Let := ∑ l ( i ∑ i ( j 2*power (power (S i) 2 + power (S j) 2) r)).

      Let : 1+(r-1)*w = power (S (power (S l) 2)) r.
      Proof. rewrite all_ones_dio; auto. Qed.

      Let : u*u = + .
      Proof.
        rewrite , Hu.
        apply const_u_square with (k' := 0) (w := 0); eauto.
      Qed.

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

      Let i : i < l 2*f i < k.
      Proof.
        unfold k, f.
        intros; rewrite power_S; apply le_n_S, power_mono_l; .
      Qed.

      Let i j : i < j < l f i < f j.
      Proof. intros; apply power_smono_l; . Qed.

      Let i1 j1 i2 j2 : < l < l f + f = f + f = = .
      Proof.
        unfold f; intros E.
        apply sum_2_power_2_injective in E; .
      Qed.

      Let : = (u*u) ⇣ w.
      Proof.
        rewrite const_u1_meet with (k := power l 2) (m := l) (f := f); auto.
        * intros i Hi; specialize ( Hi).
          revert ; unfold k; rewrite power_S; intros; .
        * rewrite power_S; auto.
      Qed.

      Let : = (u*u) ⇣ (2*w).
      Proof.
        rewrite const_u2_meet with (k := power l 2) (m := l) (f := f); auto.
        * intros i Hi; specialize ( Hi).
          revert ; unfold k; rewrite power_S; intros; .
        * rewrite power_S; auto.
     Qed.

      Let : power 2 r + = u + power (power (S l) 2) r.
      Proof.
        rewrite Hu, .
        destruct l.
        + do 2 rewrite msum_0.
          rewrite power_1; auto.
        + rewrite msum_plus1, msum_S; auto.
          rewrite power_1; ring.
      Qed.

      Let : divides (power 4 r) .
      Proof.
        rewrite .
        apply divides_msum.
        intros i _.
        apply divides_power.
        apply (@power_mono_l 2 _ 2); .
      Qed.

      Lemma const1_cn : w u2, 1+(r-1)*w = power (S (power (S l) 2)) r
                                      u*u = +
                                      = (u*u) ⇣ w
                                      = (u*u) ⇣ (2*w)
                                      power 2 r + = u + power (power (S l) 2) r
                                      divides (power 4 r) .
      Proof using Hu Hr'.
        exists w, ; repeat (split; auto).
      Qed.

    End const_1_cn.

    Section const_1_cs.

      Variable (w u : ).

      Hypothesis ( : 1+(r-1)*w = power (S (power (S l) 2)) r)
                 ( : u*u = + )
                 ( : = (u*u) ⇣ w)
                 ( : = (u*u) ⇣ (2*w))
                 ( : power 2 r + = u + power (power (S l) 2) r)
                 ( : divides (power 4 r) ).

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

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

      Let Hw : w = msum nat_join 0 (S (power (S l) 2)) ( 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)) ( i 2*power i r).
      Proof. apply all_ones_2_joins; auto. Qed.

      Let Hu1_0 : ≲ ∑ (S (power (S l) 2)) ( i 1*power i r).
      Proof. rewrite , ; auto. Qed.

      Local Lemma mk_full : { m : & { k | = ∑ (S m) ( i power (k i) r)
                                 m power (S l) 2
                                 ( i, i < S m k i power (S l) 2)
                                 i j, i < j < S m k i < k j } }.
      Proof using Hw Hu1_0 .
        assert ({ k : &
                 { g : &
                 { h | = ∑ k ( i g i * power (h i) r)
                      k S (power (S l) 2)
                      ( i, i < k g i 0 g i ≲ 1)
                      ( i, i < k h i < S (power (S l) 2))
                      ( i j, i < j < k h i < h j) } } }) as H.
        { apply (@sum_powers_binary_le_inv _ Hq' r eq_refl _ ( _ _) ( i i)); auto.
          intros; . }
        destruct H as (m' & g & h & & & & & ).
        assert ( : i, i < m' g i = 1).
        { intros i Hi; generalize ( _ Hi).
          intros (? & ); apply binary_le_le in ; . }
        assert ( : = ∑ m' ( i 1 * power (h i) r)).
        { rewrite ; apply msum_ext; intros; rewrite ; try ring; . }
        assert ( : = ∑ m' ( i power (h i) r)).
        { rewrite ; apply msum_ext; intros; ring. }
        assert ( : m' 0).
        { intros E; rewrite E, msum_0 in .
          assert (power 2 r < power (power (S l) 2) r) as C.
          { apply power_smono_l; auto.
            apply (@power_smono_l 1 _ 2); . }
          . }
        destruct m' as [ | m ]; try .
        exists m, h; repeat (split; auto).
        + .
        + intros i; generalize ( i); intros; .
      Qed.

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

      Let : = ∑ (S m) ( i power (k i) r). Proof. apply (proj2_sig ( mk_full)). Qed.
      Let Hm : m (power (S l) 2). Proof. apply (proj2_sig ( mk_full)). Qed.
      Let : i, i < S m k i power (S l) 2. Proof. apply (proj2_sig ( mk_full)). Qed.
      Let : i j, i < j < S m k i < k j. Proof. apply (proj2_sig ( mk_full)). Qed.

      Let : 4 k 0.
      Proof.
        rewrite in .
        apply power_divides_sum_power in ; auto; try .
      Qed.

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

      Let Hf1_0 : i, i S m i < S (power (S l) 2).
      Proof.
        intros [ | i ] Hi; simpl; apply le_n_S.
        + rewrite power_S.
          change 2 with (2*1) at 1.
          apply mult_le_compat; auto.
          apply power_ge_1; .
        + apply ; auto.
      Qed.

      Let Hf1_1 : i j, i < j S m i < j.
      Proof.
        intros [ | i ] [ | j ] Hij; simpl; try .
        * apply lt_le_trans with (k 0); try .
          destruct j; auto; apply lt_le_weak, ; .
        * apply ; .
      Qed.

      Let Hf1_2 : ∑ (S (S m)) ( i power ( i) r) = u + power (power (S l) 2) r.
      Proof.
        rewrite msum_S; unfold .
        rewrite ; auto.
      Qed.

      Let : k m = power (S l) 2.
      Proof.
        destruct (le_lt_dec (power (S l) 2) (k m)) as [ H | H ].
        + apply le_antisym; auto.
        + assert (∑ (S (S m)) ( i power ( i) r) < power (power (S l) 2) r); try .
          apply sum_powers_inc_lt; auto.
          - intros [ | i ] Hi; simpl.
            * apply (@power_smono_l 1 _ 2); .
            * apply le_lt_trans with (2 := H).
              destruct (eq_nat_dec i m); subst; auto.
              apply lt_le_weak, ; .
          - intros; apply Hf1_1; .
      Qed.

      Let Hu : u = ∑ (S m) ( i power ( i) r).
      Proof.
        rewrite msum_plus1 in Hf1_2; auto.
        simpl at 2 in Hf1_2.
        rewrite in Hf1_2.
        .
      Qed.

      Let Huu : u*u = ∑ (S m) ( i power (2* i) r)
                    + ∑ (S m) ( i ∑ i ( j 2*power ( i + j) r)).
      Proof.
        rewrite Hu, square_sum; f_equal.
        + apply msum_ext; intros; rewrite power_plus; f_equal; .
        + rewrite sum_0n_scal_l; apply msum_ext; intros i Hi.
          rewrite sum_0n_scal_l; apply msum_ext; intros j Hj.
          rewrite power_plus; ring.
      Qed.


      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).
        + apply mult_le_compat; auto.
          apply power_smono_l; .
        + assert (power 1 2 < power q 2) as H.
          { apply power_smono_l; . }
          rewrite power_1 in H.
          apply Nat.mul_lt_mono_pos_r; .
      Qed.

      Let Hu1_1 : { d | d S m = ∑ d ( i power (2* 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 := i i)
           as (d & & ); auto.
        + unfold r.
          apply le_lt_trans with (2*S (power (S l) 2)); try .
          apply le_lt_trans with (power (S (S (S l))) 2).
          do 4 rewrite power_S.
          * generalize (@power_ge_1 l 2); intros; .
          * apply power_smono_l; .
        + intros i Hi; generalize (@Hf1_0 i); intros; .
        + intros; apply Hf1_1; .
        + exists d; split; auto.
          rewrite , .
          apply msum_ext; intros; ring.
      Qed.

      Let Hk_final : k 0 = 4 i, i < m k (S i) = 2*k i.
      Proof.
        destruct Hu1_1 as (d & & E).
        rewrite in E.
        apply sum_powers_injective in E; auto.
        + destruct E as (? & E); subst d; split.
          * rewrite E; try ; auto.
          * intros; rewrite E; auto; .
        + intros i j H; specialize (@Hf1_1 i j); intros; .
      Qed.

      Let Hk_is_power i : i m k i = power (S (S i)) 2.
      Proof.
         induction i as [ | i IHi ]; intros Hi.
         + rewrite (proj1 Hk_final); auto.
         + rewrite (proj2 Hk_final), IHi, power_S; auto; .
      Qed.

      Let Hm_is_l : S m = l.
      Proof.
        rewrite Hk_is_power in ; auto.
        apply power_2_inj in ; .
      Qed.

      Fact obtain_u_u1_value : u = ∑ l ( i power (power (S i) 2) r)
                              = ∑ l ( i power (power (S (S i)) 2) r).
      Proof using Hu.
        split.
        + rewrite Hm_is_l, Hu.
          apply msum_ext.
          intros [ | i ]; simpl; auto.
          intros; rewrite Hk_is_power; auto; .
        + rewrite Hm_is_l, .
          apply msum_ext.
          intros [ | i ]; simpl; auto.
          * rewrite Hk_is_power; auto; .
          * intros; rewrite Hk_is_power; auto; .
      Qed.

    End const_1_cs.

  End const_1.

  Variable (l q : ).

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

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


  Lemma seqs_of_ones_dio u u1 :
            seqs_of_ones u
         l = 0 u = 0 = 0 2 q
          0 < l l+1 < q
          u2 w r0 r1 p1 p2,
                 = r
              +1 =
              = power (1+l) 2
              = power
              1+*w = *
              u*u = +
              = (u*u) ⇣ w
              = (u*u) ⇣ (2*w)
              * + = u +
              divides (***) .
  Proof.
    split.
    + intros ( & & ).
      destruct (le_lt_dec l 0) as [ | ].
      - assert (l=0) by ; subst l.
        rewrite msum_0 in , ; subst; left; .
      - right; split; auto; split; auto.
        destruct (const1_cn ) as (w & & & & & & & ).
        exists , 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; .
        * revert ; rewrite power_S, power_1; auto.
        * revert ; do 3 rewrite power_S; rewrite power_1.
          repeat rewrite mult_assoc; auto.
    + intros [ ( & & & )
             | ( & & & w & & & & & ? & & ? & ? & & & & & & ) ].
      - red; subst; do 2 rewrite msum_0; .
      - assert ( = -1) by ; clear .
        subst ; split; auto.
        apply obtain_u_u1_value with w ; auto.
        * rewrite power_S, power_1; auto.
        * do 3 rewrite power_S; rewrite power_1.
          repeat rewrite mult_assoc; auto.
  Qed.

  Definition is_cipher_of f a :=
                 l+1 < q
               ( i, i < l f i < power q 2)
               a = ∑ l ( 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.
    intros ?; unfold is_cipher_of; subst l.
    rewrite msum_0; simpl.
    repeat (split; try tauto).
    intros; .
  Qed.

  Fact is_cipher_of_inj f1 f2 a : is_cipher_of a is_cipher_of a i, i < l i = i.
  Proof.
    intros ( & & ) (_ & & ).
    rewrite in .
    revert ; apply power_decomp_unique.
    + apply (@power_mono_l 1 _ 2); .
    + intros; apply power_smono_l; .
    + intros i Hi; apply lt_le_trans with (1 := _ Hi), power_mono_l; .
    + intros i Hi; apply lt_le_trans with (1 := _ Hi), power_mono_l; .
  Qed.

  Fact is_cipher_of_fun f1 f2 a b :
          ( i, i < l i = i)
         is_cipher_of a
         is_cipher_of b
         a = b.
  Proof.
    intros (_ & _ & ) (_ & _ & ); subst a b.
    apply msum_ext; intros; f_equal; auto.
  Qed.

  Lemma is_cipher_of_equiv f1 f2 a b :
           is_cipher_of a
         is_cipher_of b
         a = b i, i < l i = i.
  Proof.
    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 ( _ 1) u
                                      l+1 < q u1, seqs_of_ones u .
  Proof.
    intros Hl.
    split.
    + intros ( & & ); split; auto.
      exists (∑ l ( i power (power (S (S i)) 2) r)).
      rewrite ; split; auto; split; auto.
      apply msum_ext; intros; ring.
    + intros ( & & _ & ).
      apply proj1 in .
      repeat (split; auto).
      * intros; apply (@power_smono_l 0); .
      * rewrite ; apply msum_ext; intros; ring.
  Qed.

  Fact is_cipher_of_u : l+1 < q is_cipher_of ( _ 1) (∑ l ( i power (power (S i) 2) r)).
  Proof.
    intros H; split; auto; split.
    + intros; apply (@power_mono_l 1 _ 2); .
    + apply msum_ext; intros; .
  Qed.

  Definition the_cipher f : l+1 < q ( i, i < l f i < power q 2) { c | is_cipher_of f c }.
  Proof.
    intros .
    exists (∑ l ( i f i * power (power (S i) 2) r)); split; auto.
  Qed.

  Definition Code a := f, is_cipher_of f a.

  Lemma Code_dio a : Code a l = 0 1 < q a = 0
                              0 < l l+1 < q p u u1, p+1 = power q 2 seqs_of_ones u a ≲ p*u.
  Proof.
    split.
    + intros (f & & & ).
      destruct (eq_nat_dec l 0) as [ Hl | Hl ].
      * left; subst l; rewrite msum_0 in ; .
      * right; split; try ; split; auto.
        exists (power q 2-1), (∑ l ( i power (power (S i) 2) r)), (∑ l ( i power (power (S (S i)) 2) r)).
        repeat (split; auto).
        - generalize (@power_ge_1 q 2); intros; .
        - rewrite .
          apply sum_power_binary_lt with (q := 4*q); auto; try .
          intros; apply power_smono_l; .
    + intros [ ( & & ) | ( & & p & & & ? & & ) ].
      * exists ( _ 0); subst a; apply is_cipher_of_0; auto.
      * destruct as (_ & & _).
        assert (p = power q 2 -1) by ; subst p.
        rewrite in .
        apply sum_power_binary_lt_inv with (q := 4*q) (e := i power (S i) 2) in ; auto; try .
        2,3: intros; apply power_smono_l; .
        destruct as (f & & ).
        exists f; split; auto.
  Qed.

  Definition Const c v := f, is_cipher_of f v 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
                                       p u u1, p = power q 2 c < p seqs_of_ones u v = c*u.
  Proof.
    split.
    + intros (f & ( & & ) & ).
      destruct (eq_nat_dec l 0) as [ Hl | Hl ].
      * left; subst l; rewrite msum_0 in ; .
      * right; split; try ; split; auto.
        exists (power q 2), (∑ l ( i power (power (S i) 2) r)), (∑ l ( i power (power (S (S i)) 2) r)).
        repeat (split; auto).
        - rewrite ( 0); try ; apply ; .
        - rewrite , sum_0n_scal_l; apply msum_ext.
          intros; f_equal; auto.
    + intros [ ( & & ) | ( & & p & & & ? & & & ) ].
      * exists ( _ 0); subst v; split.
        - apply is_cipher_of_0; auto.
        - subst l; intros; .
      * destruct as (_ & & _).
        rewrite , sum_0n_scal_l in .
        exists ( _ c); split; auto.
        split; auto; split; auto.
        intros; .
  Qed.

  Let Hr : 1 < q 4 r.
  Proof.
    intros H.
    replace (4*q) with (2*q+2*q) by .
    rewrite power_plus.
    change 4 with ((power 1 2)*(power 1 2)); apply mult_le_compat;
    apply power_mono_l; try .
  Qed.

  Section plus.

    Variable (a b c : ) (ca cb cc : )
             (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 i, i < l a i = b i + c i.
    Proof using Ha Hb Hc.
      symmetry; unfold Code_plus.
      destruct Ha as (H & & ).
      destruct Hb as (_ & & ).
      destruct Hc as (_ & & ).
      destruct (eq_nat_dec l 0) as [ | Hl ].
      + clear Hc Hb Ha. subst l; rewrite msum_0 in *; split; intros; .
      + rewrite , , , sum_0n_distr_in_out.
        split.
        * intros; apply msum_ext; intros; f_equal; auto.
        * intros E i Hi.
          apply power_decomp_unique with (i := i) in E; auto; try ; clear i Hi.
          - intros; apply power_smono_l; .
          - intros i Hi; apply lt_le_trans with (1 := _ Hi), power_mono_l; .
          - intros i Hi.
            apply lt_le_trans with (power (S q) 2).
            ++ rewrite power_S, mult_2_eq_plus.
               generalize ( _ Hi) ( _ Hi); .
            ++ apply power_mono_l; .
    Qed.

  End plus.

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

  Section mult_utils.

    Variable (b c : ) (cb cc : )
             (Hb : is_cipher_of b cb)
             (Hc : is_cipher_of c cc).

    Let : cb*cc = ∑ l ( i (b i*c i)*power (power (S (S i)) 2) r)
                       + ∑ l ( i ∑ i ( j (b i*c j + b j*c i)*power (power (S i) 2 + power (S j) 2) r)).
    Proof.
      destruct Hb as ( & & ).
      destruct Hc as (_ & & ).
      rewrite , , 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.
        apply msum_ext; intros j Hj.
        rewrite power_plus; ring.
    Qed.

    Let i : i < l b i * c i < r.
    Proof.
      destruct Hb as ( & & ).
      destruct Hc as (_ & & ).
      intro; apply mult_lt_power_2_4; auto.
    Qed.

    Let i j : i < l j < l b i * c j + b j * c i < r.
    Proof.
      destruct Hb as ( & & ).
      destruct Hc as (_ & & ).
      intros; apply mult_lt_power_2_4'; auto.
    Qed.

    Let : ∑ l ( i (b i*c i)*power (power (S (S i)) 2) r)
              = msum nat_join 0 l ( i (b i*c i)*power (power (S (S i)) 2) r).
    Proof.
      destruct Hb as ( & & ).
      destruct Hc as (_ & & ).
      apply sum_powers_ortho with (q := 4*q); try ; auto.
      intros ? ? ? ? E; apply power_2_inj in E; .
    Qed.

    Let : ∑ l ( i ∑ i ( j (b i*c j + b j*c i)*power (power (S i) 2 + power (S j) 2) r))
              = msum nat_join 0 l ( i
                           msum nat_join 0 i ( j (b i*c j + b j*c i)*power (power (S i) 2 + power (S j) 2) r)).
    Proof.
      destruct Hb as ( & & ).
      destruct Hc as (_ & & ).
      rewrite double_sum_powers_ortho with (q := 4*q); auto; try .
      + intros; apply ; .
      + intros ? ? ? ? ? ? E; apply sum_2_power_2_injective in E; .
    Qed.

    Let : cb*cc = msum nat_join 0 l ( i (b i*c i)*power (power (S (S i)) 2) r)
                      ⇡ msum nat_join 0 l ( i
                           msum nat_join 0 i ( j (b i*c j + b j*c i)*power (power (S i) 2 + power (S j) 2) r)).
    Proof.
      destruct Hb as ( & & ).
      rewrite , , .
      apply nat_ortho_plus_join.
      apply nat_ortho_joins.
      intros i j Hi Hj; apply nat_ortho_joins_left.
      intros k Hk.
      apply nat_meet_powers_neq with (q := 4*q); auto; try .
      * apply power_2_n_ij_neq; .
      * apply ; .
    Qed.

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

    Let : (r-1)*u1 = msum nat_join 0 l ( i (r-1)*power (power (S (S i)) 2) r).
    Proof.
      destruct Hb as ( & & ).
      destruct Hc as (_ & & ).
      rewrite .
      apply sum_powers_ortho with (q := 4*q); auto; try .
      intros ? ? ? ? E; apply power_2_inj in E; .
    Qed.

    Fact cipher_mult_eq : (cb*cc)⇣((r-1)*u1) = ∑ l ( i (b i*c i)*power (power (S (S i)) 2) r).
    Proof using Hb Hc.
      destruct Hb as ( & & ).
      destruct Hc as (_ & & ).
      rewrite , , .
      rewrite nat_meet_comm, nat_meet_join_distr_l.
      rewrite at 1; rewrite , .
      rewrite meet_sum_powers with (q := 4*q); auto; try (intros; ).
      2: intros; apply power_smono_l; .
      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 .
        + apply power_2_n_ij_neq; .
        + apply ; .
    Qed.

  End mult_utils.

  Section mult.

    Variable (a b c : ) (ca cb cc : )
             (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
              v v1 r' r'' p,
                        r'' = r
                      r'' = r'+1
                      seqs_of_ones v
                      p = (ca*v)⇣(r'*)
                      p = (cb*cc)⇣(r'*).

    Lemma Code_mult_spec : Code_mult i, i < l a i = b i * c i.
    Proof using Ha Hb Hc.
      unfold Code_mult; symmetry.
      destruct Ha as (Hlq & & ).
      destruct Hb as (_ & & ).
      destruct Hc as (_ & & ).
      destruct (eq_nat_dec l 0) as [ | Hl ].
      + rewrite e in *; split; intros; auto; .
      + split.
        * intros H; right; split; try .
          exists u, u1, (r-1), r, (ca * u ⇣ ((r-1) * u1)).
          split; auto; split; try .
          repeat (split; auto).
          generalize (is_cipher_of_u Hlq); intros .
          rewrite cipher_mult_eq with (1 := Ha) (2 := ).
          rewrite cipher_mult_eq with (1 := Hb) (2 := Hc).
          apply msum_ext; intros; rewrite H; try ring; .
        * intros [ | (_ & v & & r' & r'' & p & & & & & ) ]; try (destruct Hl; auto; fail).
          destruct as (_ & ? & ?); subst v .
          rewrite in .
          revert .
          generalize (is_cipher_of_u Hlq); intros .
          replace r' with (r-1) by .
          rewrite cipher_mult_eq with (1 := Ha) (2 := ).
          rewrite cipher_mult_eq with (1 := Hb) (2 := Hc).
          intros E.
          intros i Hi.
          rewrite power_decomp_unique with (5 := E); auto; try .
          - intros; apply power_smono_l; .
          - intros j Hj; rewrite Nat.mul_1_r.
            apply lt_le_trans with (1 := _ Hj), power_mono_l; .
          - intros; apply mult_lt_power_2_4; auto.
    Qed.

  End mult.

  Section inc_seq.

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

    Local Lemma IncSeq_dio_priv y : CodeNat y l = 0 1 < q y = 0
                                   0 < l
                                   z v v1,
                                        seqs_of_ones v
                                      Code y
                                      Code z
                                      y + l*(power (power (S l) 2) r) = (z*v)⇣((r-1) * )
                                      y++power (power 1 2) r = z + power (power (S l) 2) r.
    Proof.
      split.
      + intros ( & & ).
        destruct (le_lt_dec l 0) as [ | Hl ].
        - assert (l = 0) as by .
          rewrite msum_0 in ; left; .
        - right; split; auto.
          exists (∑ l ( i (S i) * power (power (S i) 2) r)), u, u1; split; auto.
          { split; auto. }
          split.
          { rewrite ; exists ( i i); split; auto. }
          split.
          { exists S; repeat (split; auto).
            intros; apply lt_le_trans with q; try .
            apply power_ge_n; auto. }
          split.
          { rewrite cipher_mult_eq with (b := S) (c := _ 1).
            * rewrite .
              rewrite msum_plus1 with (f := i i*power (power (S i) 2) r); auto.
              rewrite msum_S, Nat.mul_0_l, Nat.add_0_l.
              apply msum_ext; intros; ring.
            * repeat split; auto; intros.
              apply lt_le_trans with q; try .
              apply power_ge_n; auto.
            * apply is_cipher_of_u; auto. }
          { rewrite .
            destruct l as [ | l' ]; try .
            rewrite msum_S, Nat.mul_0_l, Nat.add_0_l.
            rewrite msum_plus1; auto.
            rewrite plus_assoc.
            rewrite msum_S.
            rewrite msum_sum; auto.
            2: intros; ring.
            rewrite Nat.mul_1_l, plus_comm.
            repeat rewrite plus_assoc; do 2 f_equal.
            apply msum_ext; intros; ring. }
      + intros [ ( & & ) | (Hl & z & v & & & & & & ) ].
        - split; subst; auto; split; intros; try .
          rewrite msum_0; auto.
        - destruct as (Hq & ? & ?); subst v .
          split; auto; split.
          { intros i Hi; apply lt_le_trans with q; try .
            apply power_ge_n; auto. }
          destruct as (f & Hf).
          destruct as (g & Hg).
          generalize (is_cipher_of_u Hq); intros Hu.
          rewrite cipher_mult_eq with (1 := Hg) (2 := Hu) in .
          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) ( i h i * power (power (S i) 2) r)) as .
          { rewrite msum_plus1; auto; f_equal.
            * rewrite Hy; apply msum_ext.
              intros i Hi; unfold h.
              destruct (le_lt_dec l i); try .
            * unfold h.
              destruct (le_lt_dec l l); try . }
          rewrite in .
          set (g' i := match i with 0 0 | S i g i end).
          assert ( ∑ (S l) ( i g' i * power (power (S i) 2) r)
                 = ∑ l ( i : g i * 1 * power (power (S (S i)) 2) r)) as .
          { unfold g'; rewrite msum_S; apply msum_ext; intros; ring. }
          rewrite in .
          assert ( i, i < S l g' i = h i) as .
          { apply power_decomp_unique with (5 := ); try .
            * intros; apply power_smono_l; .
            * unfold g'; intros [ | i ] Hi; try .
              apply lt_S_n in Hi.
              apply lt_le_trans with (1 := Hg _ Hi), power_mono_l; .
            * intros i Hi; unfold h.
              destruct (le_lt_dec l i) as [ | Hi' ].
              + apply lt_le_trans with (4*q); try .
                apply power_ge_n; auto.
              + apply lt_le_trans with (1 := Hf _ Hi'), power_mono_l; . }
          assert (h 0 = 0) as .
          { rewrite ; simpl; . }
          assert ( i, i < l h (S i) = g i) as .
          { intros i Hi; rewrite ; simpl; . }
          assert (f 0 = 0) as .
          { unfold h in ; destruct (le_lt_dec l 0); auto; . }
          assert ( i, S i < l f (S i) = g i) as .
          { intros i Hi; specialize ( i); unfold h in .
            destruct (le_lt_dec l (S i)); . }
          assert (g (l-1) = l) as .
          { specialize ( (l-1)); unfold h in .
            destruct (le_lt_dec l (S (l-1))); . }
          clear g' h .
          assert (y + u1 + power (power 1 2) r =
                  ∑ l ( i (1+f i) * power (power (S i) 2) r)
                + power (power (S l) 2) r) as .
          { rewrite sum_0n_distr_in_out.
            rewrite Hy, sum_0n_scal_l, Nat.mul_1_l.
            destruct l as [ | l' ]; try .
            rewrite msum_plus1; auto.
            rewrite msum_S; ring. }
          assert ( i, i < l 1+f i = g i) as .
          { apply power_decomp_unique with (f := i power (S i) 2) (p := r); try .
            + intros; apply power_smono_l; .
            + intros i Hi; apply le_lt_trans with (power q 2); auto.
              * apply Hf; auto.
              * apply power_smono_l; .
            + intros i Hi; apply lt_le_trans with (1 := Hg _ Hi), power_mono_l; . }
          rewrite Hy; apply msum_ext.
          clear Hy Hf Hg Hz Hu.
          intros i Hi; f_equal; revert i Hi.
          induction i as [ | i IHi ]; intros Hi; auto.
          rewrite , ; try .
    Qed.

    Lemma CodeNat_dio y : CodeNat y l = 0 1 < q y = 0
                                   0 < l
                                   z v v1 p0 p1 p2 r1,
                                         = r
                                      +1 =
                                      = power (1+l) 2
                                      = power
                                      seqs_of_ones v
                                      Code y
                                      Code z
                                      y + l* = (z*v) ⇣ ( * )
                                      y + + * = z + .
    Proof.
      rewrite IncSeq_dio_priv; split; (intros [ H | H ]; [ left | right ]); auto; revert H;
        intros ( & H); split; auto; clear ; revert H.
      + intros (z & v & & & & & & ).
        exists z, v, , r, (power (S l) 2), (power (power (S l) 2) r), (r-1); repeat (split; auto).
        * destruct ; .
        * rewrite ; f_equal.
          rewrite power_1, power_S, power_1; auto.
      + intros (z & v & & & & & & & & & & & & & & ).
        assert ( = r - 1) by ; clear ; subst.
        exists z, v, ; repeat (split; auto).
        simpl in |- *; rewrite ; f_equal.
        rewrite power_1, power_S, power_1; auto.
    Qed.

  End inc_seq.

End sums.