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