proposition: Fact list_bool_succ_nat l m : list_bool_succ l m -> 1 + list_bool_nat l = list_bool_nat m.
proof: Proof. revert l m; intros ? ? [ k l | k ]; induction k; simpl in *; lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Undecidability.Shared.Libs.DLW(Utils.utils)