fact: Fixpoint tree_foldr (T R : Type) (f : T -> R -> R) (z : R) (t : ptree T) : R := match t with | singleton x => f x z | branch ts => foldr (fun t z' => tree_foldr f z' t) z ts end.
imports: mathcomp(all_ssreflect)