proposition: Fact nat_meet_assoc n m k : n⇣(m⇣k) = n⇣m⇣k.
proof: Proof. apply equal_lb_mask_equiv; unfold nat_meet. repeat rewrite nat_lb_nat. rewrite lb_meet_assoc; 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)