proposition: Lemma mincard_le_mono n m : n <= m -> mincard n <= mincard m.
proof: Proof. induction 1; auto. transitivity (mincard m); auto using mincard_incr with arith. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)