proposition: Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1.
proof: Proof. intros; generalize (depth_max' t); destruct c; lia. Qed.
imports: Bool Arith List Program Equations(Equations) Wellfounded Arith Lia