proposition: Fact lb_pointwise_length n l m : length l <= n -> length m <= n -> length (lb_pointwise l m) <= n.
proof: Proof. revert l m; induction n as [ | n IHn ]. + intros [] []; simpl; lia. + intros [ | x l ] [ | y m ]; simpl; try rewrite map_length; auto. intros; apply le_n_S, IHn; lia. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)