proposition: Lemma id_num : forall n, num_of_nat (nat_of_num n) = n.
proof: Proof. intros n. unfold nat_of_num. pattern n. apply Pcase. simpl. reflexivity. clear n. intros n. replace (nat_of_P (Pos.succ n)) with (Datatypes.S (nat_of_P n)). simpl. apply P_of_succ_nat_o_nat_of_P_eq_succ. symmetry; apply nat_of_P_succ_morphism. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)