proposition: Fact bin_add_eq_0x0 x : bin_add ⟘ x ⟘ = (⟘,x).
proof: Proof. destruct x; auto. Qed.
imports: Arith Nat Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat bool_list gcd sums power_decomp)