proposition: Fact const_u2_meet p : p = (u*u) ⇣ (2*w) <-> p = u2.
proof: Proof. Proof using Hu1_w Hu2_2w. rewrite Hu1_u2, nat_meet_comm, nat_meet_join_distr_l. do 2 rewrite (nat_meet_comm (2*w)). rewrite Hu1_2w, Hu2_2w, nat_join_0n; tauto. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)