+theorem lt_O_to_injective_times_r: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.n*m).
+change with \forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q.
+intros 4.
+apply lt_O_n_elim n H.intros.
+apply inj_times_r m.assumption.
+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.
+