fact: Fixpoint izero_present (n:nat)(t:Z_inf_branch_tree) {struct t} :bool := match t with | Z_inf_leaf => false | Z_inf_node v f => match v with | 0 => true | _ => any_true n (fun p => izero_present n (f p)) end end.
imports: Bool ZArith