fact: Fixpoint has_zero (t: @inf_tree nat) n {struct t} : bool := match t with | Leaf => false | Node x f => (x == 0) || check_subtrees (fun s => has_zero (f s) n) n end.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq)