proposition: Fact binary_le_trans x y z : x ≲ y -> y ≲ z -> x ≲ z.
proof: Proof. do 3 rewrite binary_le_eq_lb_mask; apply lb_mask_trans. 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)