proposition: Lemma depth_max' : forall c n (t : rbtree c n), match c with | Red => depth max t <= 2 * n + 1 | Black => depth max t <= 2 * n end.
proof: Proof. intros; funelim (depth Nat.max t); auto; match goal with | [ |- context[max ?X ?Y] ] => let H := fresh in destruct (Nat.max_dec X Y) as [H|H]; rewrite H end; repeat match goal with | [ H : context[match ?C with Red => _ | Black => _ end] |- _ ] => destruct C end; lia. Qed.
imports: Bool Arith List Program Equations(Equations) Wellfounded Arith Lia