Ssrnat (p.jasmin.2025.06.1.doc.jasmin.jasmin.Jasmin.Ssrnat)

val eqn : Datatypes.nat -> Datatypes.nat -> bool

val eqnP : Datatypes.nat Eqtype.eq_axiom

val coq_HB_unnamed_factory_1 : Datatypes.nat Eqtype.Coq_hasDecEq.axioms_

val coq_Datatypes_nat__canonical__eqtype_Equality : Eqtype.Equality.coq_type

val addn_rec : Datatypes.nat -> Datatypes.nat -> Datatypes.nat

val addn : Datatypes.nat -> Datatypes.nat -> Datatypes.nat

val subn_rec : Datatypes.nat -> Datatypes.nat -> Datatypes.nat

val subn : Datatypes.nat -> Datatypes.nat -> Datatypes.nat

val leq : Datatypes.nat -> Datatypes.nat -> bool

val iter : Datatypes.nat -> ('a1 -> 'a1) -> 'a1 -> 'a1

val iteri : Datatypes.nat -> (Datatypes.nat -> 'a1 -> 'a1) -> 'a1 -> 'a1

val iterop : Datatypes.nat -> ('a1 -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1

val muln_rec : Datatypes.nat -> Datatypes.nat -> Datatypes.nat

val muln : Datatypes.nat -> Datatypes.nat -> Datatypes.nat

val expn_rec : Datatypes.nat -> Datatypes.nat -> Datatypes.nat

val expn : Datatypes.nat -> Datatypes.nat -> Datatypes.nat

val nat_of_bool : bool -> Datatypes.nat

val double_rec : Datatypes.nat -> Datatypes.nat

val double : Datatypes.nat -> Datatypes.nat