proposition: Fact nat_euclid_pow2_lb n r q : r < power n 2 -> ⟬r+q*power n 2⟭ ≂ ⟬r⟭ ↑lb_shift n ⟬q⟭ .
proof: Proof. intros H. apply lb_mask_equiv_equal. rewrite lb_nat_lb. rewrite <- lb_ortho_plus_join. 2: apply lb_shift_ortho, nat_lb_length; auto. rewrite lb_plus_spec_0; f_equal. + rewrite lb_nat_lb; auto. + rewrite lb_nat_shift, lb_nat_lb; 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)