proposition: Lemma ad_S_is_S : forall a : ad, nat_of_N (ad_S a) = S (nat_of_N a).
proof: Proof. simple induction a. reflexivity. simpl in |- *. unfold nat_of_P in |- *. intro p. exact (Pmult_nat_succ_morphism p 1). Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps)