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