proposition: Lemma mincard_incr n : mincard n < mincard (S n).
proof: Proof. induction n using lt_wf_ind. do 3 (destruct n; auto). rewrite 2 mincard_eqn. apply -> Nat.succ_lt_mono. apply Nat.add_lt_mono; eauto. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)