theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
intros.elim m.simplify.reflexivity.
simplify.
-apply trans_le ? ((S(S O))*(S n1)).
+apply (trans_le ? ((S(S O))*(S n1))).
simplify.
rewrite < plus_n_Sm.apply le_S_S.apply le_S_S.
rewrite < sym_plus.
theorem exp_to_eq_O: \forall n,m:nat. (S O) < n
\to n \sup m = (S O) \to m = O.
intros.apply antisym_le.apply le_S_S_to_le.
-rewrite < H1.change with m < n \sup m.
+rewrite < H1.change with (m < n \sup m).
apply lt_m_exp_nm.assumption.
apply le_O_n.
qed.
theorem injective_exp_r: \forall n:nat. (S O) < n \to
injective nat nat (\lambda m:nat. n \sup m).
simplify.intros 4.
-apply nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y).
-intros.apply sym_eq.apply exp_to_eq_O n.assumption.
+apply (nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y)).
+intros.apply sym_eq.apply (exp_to_eq_O n).assumption.
rewrite < H1.reflexivity.
-intros.apply exp_to_eq_O n.assumption.assumption.
+intros.apply (exp_to_eq_O n).assumption.assumption.
intros.apply eq_f.
apply H1.
(* esprimere inj_times senza S *)
-cut \forall a,b:nat.O < n \to n*a=n*b \to a=b.
+cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b).
apply Hcut.simplify. apply le_S_S_to_le. apply le_S. assumption.
assumption.
intros 2.
-apply nat_case n.
-intros.apply False_ind.apply not_le_Sn_O O H3.
+apply (nat_case n).
+intros.apply False_ind.apply (not_le_Sn_O O H3).
intros.
-apply inj_times_r m1.assumption.
+apply (inj_times_r m1).assumption.
qed.
variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.