fact: Definition insert_preserves_redblack_checker (genTree : G tree) : Checker := forAll arbitrary (fun n => forAll genTree (fun t => is_redblack_bool t ==> is_redblack_bool (insert n t))).
imports: QuickChick(QuickChick Generators) Lia mathcomp(ssreflect ssrnat ssrbool eqtype) QuickChick.RedBlack(redblack) List String