proposition: Lemma mincard_twice n : 2 * mincard n < mincard (2+n).
proof: Proof. induction n as [n IH] using lt_wf_ind. do 3 (destruct n; [simpl; auto with arith|]). change (2 + S (S (S n))) with (S (S (S (2+n)))). rewrite 2 mincard_eqn. generalize (IH n) (IH (2+n)). lia. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)