set "baseuri" "cic:/matita/nat/exp".
-include "nat/times.ma".
-include "nat/orders.ma".
-include "higher_order_defs/functions.ma".
+include "nat/div_and_mod.ma".
let rec exp n m on m\def
match m with
intros 2.
apply nat_case n.
intros.apply False_ind.apply not_le_Sn_O O H3.
-intros.apply inj_times_r m1.assumption.
+intros.
+apply inj_times_r m1.assumption.
qed.
variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
(exp p n) = (exp p m) \to n = m \def
-injective_exp_r.
-
-
+injective_exp_r.
\ No newline at end of file