proposition: Lemma bindings_aux_cardinal m acc : length acc + cardinal m = length (bindings_aux acc m).
proof: Proof. revert acc. induction m; simpl; intuition. rewrite <- IHm1; simpl. rewrite <- IHm2. rewrite Nat.add_succ_r, <- Nat.add_assoc. f_equal. f_equal. apply Nat.add_comm. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)