proposition: Lemma mincard_log n : n <= 2 * Nat.log2 (mincard n) + 1.
proof: Proof. rewrite (Nat.div2_odd n). set (m := Nat.div2 n); clearbody m. destruct (Nat.odd n); simpl Nat.b2n; rewrite ?Nat.add_0_r; clear n. + apply Nat.add_le_mono_r, Nat.mul_le_mono_l. apply Nat.log2_le_pow2. apply (@mincard_lt_mono 0); auto with arith. apply mincard_odd. + destruct (Nat.eq_dec m 0); [subst; simpl; auto|]. transitivity (2*Nat.log2 (mincard (2*m))); [|lia]. apply Nat.mul_le_mono_l. apply Nat.log2_le_pow2. apply (@mincard_lt_mono 0); lia. now apply mincard_even. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)