proposition: Lemma num_peano_rec : forall (P : num -> Type), P (num_of_nat O) -> (forall p, P p -> P (S p)) -> forall p, P p.
proof: Proof. intros P H IH p. rewrite <- id_num. generalize (nat_of_num p) as n. clear p. intros. induction n. apply H. rewrite <- (id_nat n). rewrite <- S_nat_spec. rewrite id_num. apply IH. auto. Qed.
imports: ATBR(Common) ATBR(BoolView) ATBR(MyFSets MyFSetProperties MyFMapProperties) Coq(FSetPositive FMapPositive)