proposition: Lemma le_nat_spec : forall n m, le n m <-> (nat_of_num n <= nat_of_num m)%nat.
proof: Proof. intros x y. assert (Hx := lt_O_nat_of_P x). assert (Hy := lt_O_nat_of_P y). split; intro H. assert (H' : ~nat_of_P x > nat_of_P y). unfold Pos.le in H. intro H'. apply H. apply nat_of_P_gt_Gt_compare_complement_morphism. auto. unfold nat_of_num . lia. intro H'. apply nat_of_P_gt_Gt_compare_morphism in H'. unfold nat_of_num in H. lia. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)