proposition: Lemma eqb_eq_nat_bool: forall i j, eqb i j = eq_nat_bool (nat_of_num i) (nat_of_num j).
proof: Proof. intros. num_analyse. subst. bool_simpl. reflexivity. symmetry. nat_prop. num_lia. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)