proposition: Fact lb_shift_ortho_meet n l m : length l <= n -> l ↓ lb_shift n m ≂ nil.
proof: Proof. intros; apply lb_ortho_meet_nil, lb_shift_ortho; 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)