proposition: Lemma mincard_bound n m : m <= 2+n -> mincard (S m) <= S (mincard n + mincard m).
proof: Proof. intros H. destruct m as [|[|m]]. - simpl. auto with arith. - simpl. auto with arith. - rewrite mincard_eqn. apply -> Nat.succ_le_mono. apply Nat.add_le_mono; eauto. apply mincard_le_mono; lia. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)