proposition: Fact lb_mask_equiv_equal l m : l ≂ m <-> ⟦l⟧ = ⟦m⟧.
proof: Proof. unfold lb_mask_equiv. do 2 rewrite lb_mask_eq_binary_le; split. + intros (? & ?); apply Nat.le_antisymm; apply binary_le_le; auto. + intros H; rewrite H; split; 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)