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