proposition: Lemma nat_of_num_comm : forall x y, num_of_nat y = x <-> y = nat_of_num x .
proof: Proof. intros x y. split; [intros <- | intros ->]. rewrite id_nat. reflexivity. rewrite id_num. reflexivity. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)