proposition: Fact const_u1_prefix : { q | q <= m /\ u*u ⇣ w = ∑ q (fun i => 1*power (2*f i) r) }.
proof: Proof. Proof using H2w_1 Hf1 Hf2 Hu1_u2. destruct inc_seq_split_lt with (n := m) (f := fun i => 2*f i) (k := k') as (a & H1 & H2 & H3). + intros i j Hij; apply Hf2 in Hij; lia. + exists a; split; auto. rewrite Hu1_u2, nat_meet_comm, nat_meet_join_distr_l. do 2 rewrite (nat_meet_comm w). rewrite Hu2_w, nat_join_n0. rewrite Hu1, Hw_1. replace m with (a+(m-a)) by lia. rewrite msum_plus, nat_meet_comm, nat_meet_join_distr_l. rewrite nat_join_comm. rewrite (proj2 (nat_ortho_joins k' (m-a) _ _)), nat_join_0n; auto. 3: apply nat_join_monoid. * rewrite Hseq_u; auto. rewrite nat_meet_comm. apply binary_le_nat_meet. apply nat_joins_binary_le. intros i Hi. exists (2*f i); split; auto. * intros; apply nat_meet_powers_neq with (q := 4*q); auto; try lia. generalize (H3 (a + j)); intros; lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)