proposition: 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: Proof. split. + intros (f & H1 & H2 & H3). destruct (eq_nat_dec l 0) as [ Hl | Hl ]. * left; subst l; rewrite msum_0 in H3; lia. * right; split; try lia; 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)). repeat (split; auto). - generalize (@power_ge_1 q 2); intros; lia. - rewrite H3. apply sum_power_binary_lt with (q := 4*q); auto; try lia. intros; apply power_smono_l; lia. + 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 lia; subst p. 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 lia. 2,3: intros; apply power_smono_l; lia. destruct H4 as (f & H4 & H5). exists f; split; auto. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)