proposition: Lemma S_nat_spec : forall n, nat_of_num (S n) = Datatypes.S (nat_of_num n).
proof: Proof. intros n. unfold nat_of_num. rewrite nat_of_P_succ_morphism. simpl. assert (H := lt_O_nat_of_P n). lia. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)