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