fact: Fixpoint tree_size (t : tree) : nat := match t with | Leaf => 1 | Node c tl _ tr => 1 + (tree_size tl) + (tree_size tr) end.
imports: QuickChick(QuickChick Generators) Lia mathcomp(ssreflect ssrnat ssrbool eqtype) QuickChick.RedBlack(redblack) List String