λn. λm. match_nat_type (n+1) (λp. div_aux n n p) m

Definition div : nat.nat -> nat.nat -> nat.nat := fun (n:nat.nat) => fun (m:nat.nat) => nat.match_nat_type (nat.nat) (nat.S n) (fun (p:nat.nat) => div_aux n n p) m

definition div : nat -> nat -> nat := \lambda n : nat. \lambda m : nat. (match_nat_type) (nat) ((S) n) (\lambda p : nat. (div_aux) n n p) m

noncomputable def div : (nat.nat) -> (nat.nat) -> nat.nat := fun (n : nat.nat) , fun (m : nat.nat) , ((((nat.match_nat_type) (nat.nat)) (((nat.S) ) (n))) (fun (p : nat.nat) , ((((div_mod.div_aux) ) (n)) (n)) (p))) (m)

div : [nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]] = (LAMBDA(n:nat_sttfa_th.sttfa_nat):(LAMBDA(m:nat_sttfa_th.sttfa_nat):nat_sttfa_th.match_nat_type[nat_sttfa_th.sttfa_nat](nat_sttfa_th.sttfa_S(n))((LAMBDA(p:nat_sttfa_th.sttfa_nat):div_mod_sttfa.div_aux(n)(n)(p)))(m)))

Printing for OpenTheory is not working at the moment.