proposition: Lemma lt_pi1: forall n m, lt n m -> lt (pi1 n) (pi1 m).
proof: Proof. intros n m. setoid_rewrite lt_nat_spec. unfold pi1, nat_of_num. rewrite 2 nat_of_P_xI. lia. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)