i \le n \to j \le n \to f i = f j \to i = j.
theorem injn_Sn_n: \forall f:nat \to nat. \forall n:nat.
-injn f (S n) \to injn f n.simplify.
+injn f (S n) \to injn f n.unfold injn.
intros.apply H.
apply le_S.assumption.
apply le_S.assumption.
theorem injective_to_injn: \forall f:nat \to nat. \forall n:nat.
injective nat nat f \to injn f n.
-simplify.intros.apply H.assumption.
+unfold injective.unfold injn.intros.apply H.assumption.
qed.
definition permut : (nat \to nat) \to nat \to Prop
rewrite > (not_eq_to_eqb_false k i).
rewrite > (eqb_n_n k).
simplify.reflexivity.
-simplify.intro.apply H1.apply sym_eq.assumption.
+unfold Not.intro.apply H1.apply sym_eq.assumption.
assumption.
-simplify.intro.apply H2.apply (trans_eq ? ? n).
+unfold Not.intro.apply H2.apply (trans_eq ? ? n).
apply sym_eq.assumption.assumption.
intro.apply (eqb_elim n k).intro.
simplify.
simplify.
rewrite > (eqb_n_n i).
simplify.assumption.
-simplify.intro.apply H.apply sym_eq.assumption.
+unfold Not.intro.apply H.apply sym_eq.assumption.
intro.simplify.
rewrite > (not_eq_to_eqb_false n k H5).
rewrite > (not_eq_to_eqb_false n j H4).
(f n)) m.
unfold permut.intros.
elim H.
-split.intros.simplify.
+split.intros.simplify.unfold transpose.
apply (eqb_elim (f i) (f (S m))).
intro.apply False_ind.
cut (i = (S m)).
theorem bijn_transpose : \forall n,i,j. i \le n \to j \le n \to
bijn (transpose i j) n.
-intros.simplify.intros.
+intros.unfold bijn.unfold transpose.intros.
cut (m = i \lor \lnot m = i).
elim Hcut.
apply (ex_intro ? ? j).
theorem permut_to_bijn: \forall n:nat.\forall f:nat\to nat.
permut f n \to bijn f n.
intro.
-elim n.simplify.intros.
+elim n.unfold bijn.intros.
apply (ex_intro ? ? m).
split.assumption.
apply (le_n_O_elim m ? (\lambda p. f p = p)).
apply bijn_n_Sn.
apply H.
apply permut_S_to_permut_transpose.
-assumption.simplify.
+assumption.unfold transpose.
rewrite > (eqb_n_n (f (S n1))).simplify.reflexivity.
qed.
rewrite > (not_eq_to_eqb_false (f m) (f (S n1))).
simplify.apply H2.
apply injn_Sn_n. assumption.
-simplify.intro.absurd (m = S n1).
+unfold Not.intro.absurd (m = S n1).
apply H3.apply le_S.assumption.apply le_n.assumption.
-simplify.intro.
+unfold Not.intro.
apply (not_le_Sn_n n1).rewrite < H5.assumption.
qed.
rewrite < (H1 (g (S m + n))).
apply eq_f.
apply eq_map_iter_i.
-intros.unfold transpose.
+intros.simplify.unfold transpose.
rewrite > (not_eq_to_eqb_false m1 (S m+n)).
rewrite > (not_eq_to_eqb_false m1 (S (S m)+n)).
simplify.
reflexivity.
-apply (lt_to_not_eq m1 (S (S m)+n)).
-simplify.apply le_S_S.apply le_S.assumption.
+apply (lt_to_not_eq m1 (S ((S m)+n))).
+unfold lt.apply le_S_S.change with (m1 \leq S (m+n)).apply le_S.assumption.
apply (lt_to_not_eq m1 (S m+n)).
-simplify.apply le_S_S.assumption.
+simplify.unfold lt.apply le_S_S.assumption.
qed.
theorem eq_map_iter_i_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to
rewrite > (not_eq_to_eqb_false (S (S n1)+n) i).
rewrite > (not_eq_to_eqb_false (S (S n1)+n) (S i)).
simplify.reflexivity.
-simplify.intro.
+simplify.unfold Not.intro.
apply (lt_to_not_eq i (S n1+n)).assumption.
apply inj_S.apply sym_eq. assumption.
-simplify.intro.
-apply (lt_to_not_eq i (S (S n1+n))).simplify.
+simplify.unfold Not.intro.
+apply (lt_to_not_eq i (S (S n1+n))).simplify.unfold lt.
apply le_S_S.assumption.
apply sym_eq. assumption.
apply H2.assumption.apply le_S_S_to_le.
intros.
apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n)).
apply H2.
-simplify. apply le_n.assumption.
+unfold lt. apply le_n.assumption.
apply (trans_le ? (S(S (m1+i)))).
apply le_S.apply le_n.assumption.
apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n)).
apply (H2 O ? ? (S(m1+i))).
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
apply (trans_le ? i).assumption.
change with (i \le (S m1)+i).apply le_plus_n.
exact H4.
(transpose (S(m1 + i)) (S(S(m1 + i)))
(transpose i (S(m1 + i)) m)))) f n)).
apply (H2 m1).
-simplify. apply le_n.assumption.
+unfold lt. apply le_n.assumption.
apply (trans_le ? (S(S (m1+i)))).
apply le_S.apply le_n.assumption.
apply eq_map_iter_i.
intros.apply eq_f.
apply sym_eq. apply eq_transpose.
-simplify. intro.
+unfold Not. intro.
apply (not_le_Sn_n i).
rewrite < H7 in \vdash (? ? %).
apply le_S_S.apply le_S.
apply le_plus_n.
-simplify. intro.
+unfold Not. intro.
apply (not_le_Sn_n i).
rewrite > H7 in \vdash (? ? %).
apply le_S_S.
apply le_plus_n.
-simplify. intro.
+unfold Not. intro.
apply (not_eq_n_Sn (S m1+i)).
apply sym_eq.assumption.
qed.
simplify.apply H4.assumption.
rewrite > H4.
apply lt_to_not_eq.apply (trans_lt ? n1).assumption.
-simplify.apply le_S_S.apply le_plus_n.assumption.
+simplify.unfold lt.apply le_S_S.apply le_plus_n.assumption.
unfold permut in H3.elim H3.
-simplify.intro.
+simplify.unfold Not.intro.
apply (lt_to_not_eq m (S n+n1)).apply (trans_lt ? n1).assumption.
-simplify.apply le_S_S.apply le_plus_n.
+simplify.unfold lt.apply le_S_S.apply le_plus_n.
unfold injn in H7.
apply (H7 m (S n+n1)).apply (trans_le ? n1).
apply lt_to_le.assumption.apply le_plus_n.apply le_n.