fact: Fixpoint has_no_red_red (c : color) (t : tree) : bool := match t with | Leaf => true | Node Red t1 _ t2 => match c with | Red => false | Black => has_no_red_red Red t1 && has_no_red_red Red t2 end | Node Black t1 _ t2 => has_no_red_red Black t1 && has_no_red_red Black t2 end.
imports: QuickChick(QuickChick Generators) Lia mathcomp(ssreflect ssrnat ssrbool eqtype) QuickChick.RedBlack(redblack) List String