λn. λm. (mod m n) = O

Definition dividesb : nat.nat -> nat.nat -> bool.bool := fun (n:nat.nat) => fun (m:nat.nat) => nat.eqb (div_mod.mod m n) nat.O

definition dividesb : nat -> nat -> bool := \lambda n : nat. \lambda m : nat. (eqb) ((mod) m n) (O)

noncomputable def dividesb : (nat.nat) -> (nat.nat) -> bool.bool := fun (n : nat.nat) , fun (m : nat.nat) , (((nat.eqb) ) ((((div_mod.mod) ) (m)) (n))) ((nat.O) )

dividesb : [nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]] = (LAMBDA(n:nat_sttfa_th.sttfa_nat):(LAMBDA(m:nat_sttfa_th.sttfa_nat):nat_sttfa_th.eqb(div_mod_sttfa_th.mod(m)(n))(nat_sttfa_th.sttfa_O)))

Printing for OpenTheory is not working at the moment.