proposition: Lemma elements_aux_cardinal : forall s acc, (length acc + cardinal s)%nat = length (elements_aux acc s).
proof: Proof. simple induction s; simpl; intuition. rewrite <- H. simpl. rewrite <- H0. rewrite (Nat.add_comm (cardinal t0)). now rewrite <- Nat.add_succ_r, Nat.add_assoc. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat