proposition: Fact div2_spec n : match div2 n with | (p,One) => n = 2*p+1 | (p,Zero) => n = 2*p end.
proof: Proof. induction n as [ [ | [ | n ] ] IHn ] using (well_founded_induction lt_wf); simpl; auto. specialize (IHn n). destruct (div2 n) as (p,[]); simpl in * |- *; lia. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)