qed.
variant inj_times_r1:\forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q
\def lt_O_to_injective_times_r.
theorem injective_times_l: \forall n:nat.injective nat nat (\lambda m:nat.m*(S n)).
qed.
variant inj_times_r1:\forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q
\def lt_O_to_injective_times_r.
theorem injective_times_l: \forall n:nat.injective nat nat (\lambda m:nat.m*(S n)).