proposition: Lemma lt_nat_spec : forall n m, lt 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. assert (nat_of_P x < nat_of_P y). apply nat_of_P_lt_Lt_compare_morphism. apply H. unfold nat_of_num. lia. apply nat_of_P_lt_Lt_compare_complement_morphism. unfold nat_of_num in H. lia. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)