proposition: Lemma mincard_odd n : 2^n <= mincard (2*n+1).
proof: Proof. destruct (Nat.eq_dec n 0). - subst; auto. - transitivity (mincard (2*n)). * now apply mincard_even. * apply mincard_le_mono. lia. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)