proposition: Lemma maxdepth_cardinal m : cardinal m < 2^(maxdepth m).
proof: Proof. unfold Peano.lt. induction m as [|c l IHl x e r IHr]. - auto. - simpl. rewrite <- Nat.add_succ_r, <- Nat.add_succ_l, Nat.add_0_r. apply Nat.add_le_mono; etransitivity; try apply IHl; try apply IHr; apply Nat.pow_le_mono; auto. * apply Nat.le_max_l. * apply Nat.le_max_r. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)