proposition: Lemma leb_false : forall x y, leb x y = false <-> lt y x.
proof: Proof. intros. rewrite eq_not_negb. rewrite leb_true. rewrite le_nat_spec, lt_nat_spec. lia. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)