proposition: Lemma lb_mask_eq_binary_le l m : l ⪯ m <-> ⟦l⟧ ≲ ⟦m⟧.
proof: Proof. split; auto; intro. rewrite <- (lb_mask_nat l), <- (lb_mask_nat m); 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)