proposition: Lemma has_black_height : forall t h c, is_redblack' t c h -> black_height_bool t = Some h.
proof: Proof. elim => [| c t1 IHt1 n t2 IHt2] h c' Hrb; first by inversion Hrb. inversion Hrb as [| n' tl tr h' Htl Htr | c'' n' tl tr h' Htl Htr]; subst; move: Htl Htr => /IHt1 Htl /IHt2 Htr; simpl; by rewrite Htl Htr eq_refl. Qed.
imports: mathcomp(ssreflect ssrnat ssrbool eqtype) List String Lia QuickChick(QuickChick) QuickChick.RedBlack(redblack testing)