proposition: Lemma num_of_nat_comm : forall x y, x = num_of_nat y <-> nat_of_num x = y.
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)