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

Theorem

nat.commutative_plus

Statement

commutative plus

Main Dependencies
Theory
Coq-Jumb
Statement

Theorem commutative_plus : relations.commutative (nat) plus.


Matita-Jumb
Statement

theorem commutative_plus : (commutative) (nat) (plus) .


Lean-jumb
Statement

theorem commutative_plus : ((relations.commutative) (nat.nat)) ((nat.plus) ).


PVS-jumb
Statement

commutative_plus : LEMMA relations_sttfa_th.commutative[nat_sttfa.sttfa_nat](nat_sttfa.plus)


OpenTheory

Printing for OpenTheory is not working at the moment.