proposition: Lemma nat_meet_mult_power2 q x y : (x*power q 2) ⇣ (y*power q 2) = (x⇣y)*power q 2.
proof: Proof. unfold nat_meet. rewrite <- lb_nat_shift, lb_shift_meet. apply lb_mask_equiv_equal. do 2 rewrite nat_pow2_lb_shift; 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)