proposition: Fact lb_shift_meet n l m : lb_shift n (l↓m) = (lb_shift n l)↓(lb_shift n m).
proof: Proof. induction n as [ | n IHn ]. + repeat rewrite lb_shift_0; auto. + do 3 rewrite lb_shift_S. rewrite lb_meet_cons; f_equal; 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)