proposition: Fact nat_join_idem n : n⇡n = n.
proof: Proof. apply equal_lb_mask_equiv. unfold nat_join. rewrite nat_lb_nat, lb_join_idem; 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)