proposition: Fact lb_mask_binary_le l m : l ⪯ m -> ⟦l⟧ ≲ ⟦m⟧.
proof: Proof. induction 1 as [ l | l H1 IH1 | x y l m H1 H2 IH2 ]. - constructor 1. - apply binary_le_zero_inv in IH1. simpl; rewrite IH1; constructor. - do 2 rewrite lb_nat_fix_3. constructor 2. * do 2 rewrite rem_2_bool2nat. revert x y H1; intros [] []; simpl; auto; discriminate. * do 2 rewrite div_2_bool2nat; 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)