proposition: Lemma is_redblackP t : reflect (is_redblack t) (is_redblack_bool t).
proof: Proof. apply (@iffP (is_redblack_bool t)); first by apply/idP. rewrite /is_redblack_bool. + move => /andP [Hb Hrr]. rewrite /is_black_balanced in Hb. have [h Hbh] : exists h, black_height_bool t = Some h by destruct (black_height_bool t) => //; eexists. exists h. apply/is_redblack'P. apply/andP; split => //; apply/eqP => //. + move => [h /is_redblack'P /andP [/eqP H1 H2]]. rewrite /is_redblack_bool /is_black_balanced H1. apply/andP; split => //. Qed.
imports: mathcomp(ssreflect ssrnat ssrbool eqtype) List String Lia QuickChick(QuickChick) QuickChick.RedBlack(redblack testing)