proposition: Lemma well_founded_hc : well_founded wf_hc.
proof: Proof. unfold wf_hc. apply wf_inverse_image. apply wf_lexprod. now apply Wf_nat.lt_wf. intros _; now apply well_foulded_ltColor. Qed.
imports: QuickChick(QuickChick Generators) Lia mathcomp(ssreflect ssrnat ssrbool eqtype) QuickChick.RedBlack(redblack) List String Relations Wellfounded Lexicographic_Product