proposition: Lemma well_foulded_ltColor : well_founded ltColor.
proof: Proof. unfold well_founded. intros c; destruct c; repeat (constructor; intros c ?; destruct c; try now (exfalso; auto)). Qed.
imports: QuickChick(QuickChick Generators) Lia mathcomp(ssreflect ssrnat ssrbool eqtype) QuickChick.RedBlack(redblack) List String Relations Wellfounded Lexicographic_Product