proposition: Fact const_u1_eq : (u*u) ⇣ w = u1.
proof: Proof. Proof using Hu1_w. apply const_u1_meet; auto. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)