proposition: Fact nat_join_eq_0 n m : n⇡m = 0 <-> n = 0 /\ m = 0.
proof: Proof. split. + do 3 rewrite equal_lb_mask_equiv. unfold nat_join; rewrite nat_lb_nat. repeat rewrite nat_lb_fix_0. apply lb_join_nil_eq. + intros []; subst; apply nat_join_0n. 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)