proposition: Lemma fold_plus : forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p.
proof: Proof. intros. apply fold_rel with (R:=fun u v => u = v + p); simpl; auto. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide