proposition: 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: 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; lia. * rewrite <- H5; f_equal. 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 lia; clear H2; subst. exists z, v, v1; repeat (split; auto). simpl in H9 |- *; rewrite <- H9; f_equal. rewrite power_1, power_S, power_1; auto. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)