fact: Fixpoint div2 n : nat * bool := match n with | 0 => (0,Zero) | 1 => (0,One) | S (S n) => let (p,b) := div2 n in (S p,b) end.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)