proposition: Theorem depth_min : forall c n (t : rbtree c n), depth min t >= n.
proof: Proof. intros. funelim (depth Nat.min t); auto; match goal with | [ |- context[min ?X ?Y] ] => let H := fresh in destruct (Nat.min_dec X Y) as [H|H]; rewrite H end; lia. Qed.
imports: Bool Arith List Program Equations(Equations) Wellfounded Arith Lia