rewrite < H.
rewrite > (S_pred ((S n1)*(S m))).
apply sigma_plus1.
-simplify.apply le_S_S.apply le_O_n.
+simplify.unfold lt.apply le_S_S.apply le_O_n.
qed.
theorem eq_sigma_sigma1 : \forall n,m:nat.\forall f:nat \to nat.
((i1*(S n) + i) \mod (S n)) i1 i).
rewrite > H3.
apply bool_to_nat_andb.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
apply div_mod_spec_div_mod.
-simplify.apply le_S_S.apply le_O_n.
-constructor 1.simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+constructor 1.unfold lt.apply le_S_S.assumption.
reflexivity.
apply div_mod_spec_div_mod.
-simplify.apply le_S_S.apply le_O_n.
-constructor 1.simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+constructor 1.unfold lt.apply le_S_S.assumption.
reflexivity.
apply (trans_eq ? ?
(sigma n (\lambda n.((bool_to_nat (f1 n)) *
change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
apply H.
apply lt_mod_m_m.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
apply (lt_times_to_lt_l n).
apply (le_to_lt_to_lt ? i).
rewrite > (div_mod i (S n)) in \vdash (? ? %).
rewrite > sym_plus.
apply le_plus_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
unfold lt.
rewrite > S_pred in \vdash (? ? %).
apply le_S_S.
rewrite > sym_times. assumption.
rewrite > (times_n_O O).
apply lt_times.
-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
rewrite > (times_n_O O).
apply lt_times.
-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
rewrite < plus_n_O.
unfold injn.
intros.
rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
rewrite > H6.reflexivity.
-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
apply (lt_times_to_lt_l n).
apply (le_to_lt_to_lt ? j).
rewrite > (div_mod j (S n)) in \vdash (? ? %).
rewrite > sym_plus.
apply le_plus_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
rewrite < sym_times. assumption.
apply lt_mod_m_m.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
apply (lt_times_to_lt_l n).
apply (le_to_lt_to_lt ? i).
rewrite > (div_mod i (S n)) in \vdash (? ? %).
rewrite > sym_plus.
apply le_plus_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
rewrite < sym_times. assumption.
apply lt_mod_m_m.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
unfold lt.
rewrite > S_pred in \vdash (? ? %).
apply le_S_S.assumption.
rewrite > (times_n_O O).
apply lt_times.
-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
unfold lt.
rewrite > S_pred in \vdash (? ? %).
apply le_S_S.assumption.
rewrite > (times_n_O O).
apply lt_times.
-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
intros.
apply False_ind.
apply (not_le_Sn_O m1 H4).