fact: Fixpoint black_height_bool (t: tree) : option nat := match t with | Leaf => Some 0 | Node c tl _ tr => let h1 := black_height_bool tl in let h2 := black_height_bool tr in match h1, h2 with | Some n1, Some n2 => if n1 == n2 then match c with | Black => Some (S n1) | Red => Some n1 end else None | _, _ => None end end.
imports: QuickChick(QuickChick Generators) Lia mathcomp(ssreflect ssrnat ssrbool eqtype) QuickChick.RedBlack(redblack) List String