proposition: Lemma max_spec : forall n m, nat_of_num (max n m) = Nat.max (nat_of_num n) (nat_of_num m).
proof: Proof. intros n m. unfold max, Pos.max. fold (compare n m). destruct (compare_spec n m). rewrite Nat.max_r; trivial. apply Nat.lt_le_incl. rewrite <- lt_nat_spec. assumption. subst. rewrite Nat.max_r; trivial. rewrite Nat.max_l; trivial. apply Nat.lt_le_incl. rewrite <- lt_nat_spec. assumption. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)