proposition: Lemma fold_num_S: forall A (a: A) f n, fold_num f (S n) a = fold_num f n (f n a).
proof: Proof. intros. unfold fold_num at 1. rewrite Prect_succ. reflexivity. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)