proposition: 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: Proof. split. + intros (f & (H1 & H2 & H3) & H4). 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), (∑ l (fun i => power (power (S i) 2) r)), (∑ l (fun i => power (power (S (S i)) 2) r)). repeat (split; auto). - rewrite <- (H4 0); try lia; apply H2; lia. - rewrite H3, <- sum_0n_scal_l; apply msum_ext. 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; lia. * destruct H4 as (_ & H4 & _). rewrite H4, <- sum_0n_scal_l in H5. exists (fun _ => c); split; auto. split; auto; split; auto. intros; lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)