proposition: Fact lb_shift_ortho n l m : length l <= n -> l ⟂ lb_shift n m.
proof: Proof. revert n. induction l as [ | x l IHl ]; intros [ | n ]; simpl; auto; try lia. intro; rewrite lb_shift_S; constructor; auto; apply IHl; lia. 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)