proposition: Lemma mincard_even n : n<>0 -> 2^n <= mincard (2*n).
proof: Proof. induction n. - now destruct 1. - intros _. destruct (Nat.eq_dec n 0). * subst; simpl; auto. * rewrite Nat.pow_succ_r', Nat.mul_succ_r, Nat.add_comm. transitivity (2 * mincard (2*n)). + apply Nat.mul_le_mono_l; auto. + apply Nat.lt_le_incl. apply mincard_twice. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)