proposition: Lemma is_redblack'P : forall (t : tree) n c, reflect (is_redblack' t c n) ((black_height_bool t == Some n) && has_no_red_red c t).
proof: Proof. elim => [| c t1 IHt1 n t2 IHt2] n' c'. - simpl. apply (@iffP ((Some 0 == Some n') && true)); first by apply/idP. + move => /andP [/eqP [H1] _]; subst. econstructor. + move => Hrb. apply/andP. inversion Hrb; subst. split => //. - apply (@iffP ((black_height_bool (Node c t1 n t2) == Some n') && has_no_red_red c' (Node c t1 n t2))); first by apply/idP. + move => /andP [/eqP /= H1 H2]; subst. destruct (black_height_bool t1) eqn:Heqh1, (black_height_bool t2) eqn:Heqh2; (try discriminate). have Heq : (n0 = n1) by apply/eqP; destruct (n0 == n1). subst. rewrite eq_refl in H1. destruct c; inversion H1; subst; clear H1; destruct c' => //=; move : H2 => /andP [Ht1 Ht2]; (constructor; [apply/IHt1 | apply/IHt2]); apply/andP; split => //. + move => Hrb. inversion Hrb as [| n'' tl tr h Hrbl Hrbr | c'' n'' tl tr h Hrbl Hrbr]; subst; move: Hrbl Hrbr => /IHt1/andP [/eqP Hbhl Hrrl] /IHt2/andP [/eqP Hbhr Hrrr]; apply/andP; split => //; simpl; (try by rewrite Hbhl Hbhr eq_refl); by (apply/andP; split => //). Qed.
imports: mathcomp(ssreflect ssrnat ssrbool eqtype) List String Lia QuickChick(QuickChick) QuickChick.RedBlack(redblack testing)