fact: Definition wf_hc (c1 c2 : (nat * color)) : Prop := lexprod nat (fun _ => color) lt (fun _ => ltColor) (sigT_of_prod c1) (sigT_of_prod c2).
imports: QuickChick(QuickChick Generators) Lia mathcomp(ssreflect ssrnat ssrbool eqtype) QuickChick.RedBlack(redblack) List String Relations Wellfounded Lexicographic_Product