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

Theorem

nat.injective_plus_r

Statement

∀ n, injective (λm. n + m)

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem injective_plus_r : forall (n:nat), relations.injective (nat) (nat) (fun (m:nat) => plus n m).



Matita-Jumb
Statement

theorem injective_plus_r : \forall (n:nat). (injective) (nat) (nat) (\lambda m : nat. (plus) n m).



Lean-jumb
Statement

theorem injective_plus_r : forall (n:nat.nat) , ((relations.injective) (nat.nat) (nat.nat)) (fun (m : nat.nat) , (((nat.plus) ) (n)) (m)).



PVS-jumb

Statement

injective_plus_r : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):relations_sttfa_th.injective[nat_sttfa.sttfa_nat,nat_sttfa.sttfa_nat]((LAMBDA(m:nat_sttfa.sttfa_nat):nat_sttfa.plus(n)(m))))



OpenTheory

Printing for OpenTheory is not working at the moment.