proposition: Lemma id_nat : forall n, nat_of_num (num_of_nat n) = n.
proof: Proof. intros n. unfold nat_of_num. assert (Hn : 0 < nat_of_P (num_of_nat n) ). apply lt_O_nat_of_P. assert (forall s n, 0 <s -> s = Datatypes.S n -> pred s = n). intros. lia. apply H. auto. apply nat_of_P_o_P_of_succ_nat_eq_succ. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)