-sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g.
-intros 4.
-elim n
- [generalize in match H5.
- elim n1
- [reflexivity
- |apply (bool_elim ? (p2 n2));intro
- [apply False_ind.
- apply (not_le_Sn_O (h1 n2)).
- apply H7
- [apply le_n|assumption]
- |rewrite > false_to_sigma_p_Sn
- [apply H6.
- intros.
- apply H7[apply le_S.apply H9|assumption]
- |assumption
- ]
- ]
- ]
- |apply (bool_elim ? (p1 n1));intro
- [rewrite > true_to_sigma_p_Sn
- [rewrite > (sigma_p_gi g n2 (h n1))
- [apply eq_f2
- [reflexivity
- |apply H
- [intros.
- rewrite > H1
- [simplify.
- change with ((\not eqb (h i) (h n1))= \not false).
- apply eq_f.
- apply not_eq_to_eqb_false.
- unfold Not.intro.
- apply (lt_to_not_eq ? ? H8).
- rewrite < H2
- [rewrite < (H2 n1)
- [apply eq_f.assumption|apply le_n|assumption]
- |apply le_S.assumption
- |assumption
- ]
- |apply le_S.assumption
- |assumption
- ]
- |intros.
- apply H2[apply le_S.assumption|assumption]
- |intros.
- apply H3[apply le_S.assumption|assumption]
- |intros.
- apply H4
- [assumption
- |generalize in match H9.
- elim (p2 j)
- [reflexivity|assumption]
- ]
- |intros.
- apply H5
- [assumption
- |generalize in match H9.
- elim (p2 j)
- [reflexivity|assumption]
- ]
- |intros.
- elim (le_to_or_lt_eq (h1 j) n1)
- [assumption
- |generalize in match H9.
- elim (p2 j)
- [simplify in H11.
- absurd (j = (h n1))
- [rewrite < H10.
- rewrite > H5
- [reflexivity|assumption|auto]
- |apply eqb_false_to_not_eq.
- generalize in match H11.
- elim (eqb j (h n1))
- [apply sym_eq.assumption|reflexivity]
- ]
- |simplify in H11.
- apply False_ind.
- apply not_eq_true_false.
- apply sym_eq.assumption
- ]
- |apply le_S_S_to_le.
- apply H6
- [assumption
- |generalize in match H9.
- elim (p2 j)
- [reflexivity|assumption]
- ]
- ]
- ]
- ]
- |apply H3[apply le_n|assumption]
- |apply H1[apply le_n|assumption]
- ]
- |assumption
- ]
- |rewrite > false_to_sigma_p_Sn
- [apply H
- [intros.apply H1[apply le_S.assumption|assumption]
- |intros.apply H2[apply le_S.assumption|assumption]
- |intros.apply H3[apply le_S.assumption|assumption]
- |intros.apply H4[assumption|assumption]
- |intros.apply H5[assumption|assumption]
- |intros.
- elim (le_to_or_lt_eq (h1 j) n1)
- [assumption
- |absurd (j = (h n1))
- [rewrite < H10.
- rewrite > H5
- [reflexivity|assumption|assumption]
- |unfold Not.intro.
- apply not_eq_true_false.
- rewrite < H7.
- rewrite < H10.
- rewrite > H4
- [reflexivity|assumption|assumption]
- ]
- |apply le_S_S_to_le.
- apply H6[assumption|assumption]
- ]
- ]
- |assumption
- ]
- ]
- ]
-qed.
-
-definition p_ord_times \def
-\lambda p,m,x.
- match p_ord x p with
- [pair q r \Rightarrow r*m+q].
-
-theorem eq_p_ord_times: \forall p,m,x.
-p_ord_times p m x = (ord_rem x p)*m+(ord x p).
-intros.unfold p_ord_times. unfold ord_rem.
-unfold ord.
-elim (p_ord x p).
-reflexivity.
-qed.
-
-theorem div_p_ord_times:
-\forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
-intros.rewrite > eq_p_ord_times.
-apply div_plus_times.
-assumption.
-qed.
-
-theorem mod_p_ord_times:
-\forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
-intros.rewrite > eq_p_ord_times.
-apply mod_plus_times.
-assumption.
-qed.
-
-theorem times_O_to_O: \forall n,m:nat.n*m = O \to n = O \lor m= O.
-apply nat_elim2;intros
- [left.reflexivity
- |right.reflexivity
- |apply False_ind.
- simplify in H1.
- apply (not_eq_O_S ? (sym_eq ? ? ? H1))
- ]