proposition: Lemma cardinal_spec: forall s, cardinal s = length (elements s).
proof: Proof. unfold elements. assert (H: forall s j acc, (cardinal s + length acc)%nat = length (xelements s j acc)). - induction s as [|l IHl b r IHr]; intros j acc; simpl; trivial. destruct b. + rewrite <- IHl. simpl. rewrite <- IHr. rewrite <- plus_n_Sm, Nat.add_assoc. reflexivity. + rewrite <- IHl, <- IHr. rewrite Nat.add_assoc. reflexivity. - intros. rewrite <- H. simpl. rewrite Nat.add_comm. reflexivity. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface