proposition: Fact cipher_mult_eq : (cb*cc)⇣((r-1)*u1) = ∑ l (fun i => (b i*c i)*power (power (S (S i)) 2) r).
proof: Proof. Proof using Hb Hc. destruct Hb as (H1 & Hb1 & Hb2). destruct Hc as (_ & Hc1 & Hc2). rewrite eq2, Hbc_3, Hr_2. rewrite nat_meet_comm, nat_meet_join_distr_l. rewrite <- Hr_2 at 1; rewrite Hr_1, <- Hbc_3. rewrite meet_sum_powers with (q := 4*q); auto; try (intros; lia). 2: intros; apply power_smono_l; lia. 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 lia. + apply power_2_n_ij_neq; lia. + apply Hbc_2; lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)