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