// This prints the left floatting menu
Dedukti    Load Matita      Load Coq         Load Lean        Load PVS         Load OpenTheory Load
Dedukti-jumb

Theorem

div_mod.eq_div_aux_body_O

Statement

leibniz (div_aux_body O) (λm. λn. O)

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem eq_div_aux_body_O : leibniz.leibniz (nat.nat -> nat.nat -> nat.nat) (div_aux_body nat.O) (fun (m:nat.nat) => fun (n:nat.nat) => nat.O).



Matita-Jumb
Statement

theorem eq_div_aux_body_O : (leibniz) (nat -> nat -> nat) ((div_aux_body) (O) ) (\lambda m : nat. \lambda n : nat. (O) ).



Lean-jumb
Statement

theorem eq_div_aux_body_O : (((leibniz.leibniz) ((nat.nat) -> (nat.nat) -> nat.nat)) (((div_mod.div_aux_body) ) ((nat.O) ))) (fun (m : nat.nat) , fun (n : nat.nat) , (nat.O) ).



PVS-jumb

Statement

eq_div_aux_body_O : LEMMA leibniz_sttfa_th.leibniz[[nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]]](div_mod_sttfa.div_aux_body(nat_sttfa_th.sttfa_O))((LAMBDA(m:nat_sttfa_th.sttfa_nat):(LAMBDA(n:nat_sttfa_th.sttfa_nat):nat_sttfa_th.sttfa_O)))



OpenTheory

Printing for OpenTheory is not working at the moment.