sigma_p (S n)
(\lambda d.divides_b d n) (\lambda d. (f d)*(g (div n d))).
-(* da spostare *)
-
-(* spostati in div_and_mod.ma
-theorem mod_SO: \forall n:nat. mod n (S O) = O.
-intro.
-apply sym_eq.
-apply le_n_O_to_eq.
-apply le_S_S_to_le.
-apply lt_mod_m_m.
-apply le_n.
-qed.
-theorem div_SO: \forall n:nat. div n (S O) = n.
-intro.
-rewrite > (div_mod ? (S O)) in \vdash (? ? ? %)
- [rewrite > mod_SO.
- rewrite < plus_n_O.
- apply times_n_SO
- |apply le_n
- ]
-qed.*)
-
-theorem and_true: \forall a,b:bool.
-andb a b =true \to a =true \land b= true.
-intro.elim a
- [split
- [reflexivity|assumption]
- |apply False_ind.
- apply not_eq_true_false.
- apply sym_eq.
- assumption
- ]
-qed.
-
-theorem lt_times_plus_times: \forall a,b,n,m:nat.
-a < n \to b < m \to a*m + b < n*m.
-intros 3.
-apply (nat_case n)
- [intros.apply False_ind.apply (not_le_Sn_O ? H)
- |intros.simplify.
- rewrite < sym_plus.
- unfold.
- change with (S b+a*m1 \leq m1+m*m1).
- apply le_plus
- [assumption
- |apply le_times
- [apply le_S_S_to_le.assumption
- |apply le_n
- ]
- ]
- ]
-qed.
-
-theorem divides_to_divides_b_true1 : \forall n,m:nat.
-O < m \to n \divides m \to divides_b n m = true.
-intro.
-elim (le_to_or_lt_eq O n (le_O_n n))
- [apply divides_to_divides_b_true
- [assumption|assumption]
- |apply False_ind.
- rewrite < H in H2.
- elim H2.
- simplify in H3.
- apply (not_le_Sn_O O).
- rewrite > H3 in H1.
- assumption
- ]
-qed.
-(* spostato in primes.ma
-theorem divides_to_div: \forall n,m.divides n m \to m/n*n = m.
-intro.
-elim (le_to_or_lt_eq O n (le_O_n n))
- [rewrite > plus_n_O.
- rewrite < (divides_to_mod_O ? ? H H1).
- apply sym_eq.
- apply div_mod.
- assumption
- |elim H1.
- generalize in match H2.
- rewrite < H.
- simplify.
- intro.
- rewrite > H3.
- reflexivity
- ]
-qed.*)
-(* spostato in div_and_mod.ma
-theorem le_div: \forall n,m. O < n \to m/n \le m.
-intros.
-rewrite > (div_mod m n) in \vdash (? ? %)
- [apply (trans_le ? (m/n*n))
- [rewrite > times_n_SO in \vdash (? % ?).
- apply le_times
- [apply le_n|assumption]
- |apply le_plus_n_r
- ]
- |assumption
- ]
-qed.*)
-
-theorem sigma_p2_eq:
-\forall g: nat \to nat \to Z.
-\forall h11,h12,h21,h22: nat \to nat \to nat.
-\forall n,m.
-\forall p11,p21:nat \to bool.
-\forall p12,p22:nat \to nat \to bool.
-(\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
-p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
-\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
-\land h11 i j < n \land h12 i j < m) \to
-(\forall i,j. i < n \to j < m \to p11 i = true \to p12 i j = true \to
-p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
-\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
-\land (h21 i j) < n \land (h22 i j) < m) \to
-sigma_p n p11 (\lambda x:nat .sigma_p m (p12 x) (\lambda y. g x y)) =
-sigma_p n p21 (\lambda x:nat .sigma_p m (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
-intros.
-rewrite < sigma_p2'.
-rewrite < sigma_p2'.
-apply sym_eq.
-letin h := (\lambda x.(h11 (x/m) (x\mod m))*m + (h12 (x/m) (x\mod m))).
-letin h1 := (\lambda x.(h21 (x/m) (x\mod m))*m + (h22 (x/m) (x\mod m))).
-apply (trans_eq ? ?
- (sigma_p (n*m) (\lambda x:nat.p21 (x/m)\land p22 (x/m) (x\mod m))
- (\lambda x:nat.g ((h x)/m) ((h x)\mod m))))
- [clear h.clear h1.
- apply eq_sigma_p1
- [intros.reflexivity
- |intros.
- cut (O < m)
- [cut (x/m < n)
- [cut (x \mod m < m)
- [elim (and_true ? ? H3).
- elim (H ? ? Hcut1 Hcut2 H4 H5).
- elim H6.clear H6.
- elim H8.clear H8.
- elim H6.clear H6.
- elim H8.clear H8.
- apply eq_f2
- [apply sym_eq.
- apply div_plus_times.
- assumption
- |autobatch
- ]
- |apply lt_mod_m_m.
- assumption
- ]
- |apply (lt_times_n_to_lt m)
- [assumption
- |apply (le_to_lt_to_lt ? x)
- [apply (eq_plus_to_le ? ? (x \mod m)).
- apply div_mod.
- assumption
- |assumption
- ]
- ]
- ]
- |apply not_le_to_lt.unfold.intro.
- generalize in match H2.
- apply (le_n_O_elim ? H4).
- rewrite < times_n_O.
- apply le_to_not_lt.
- apply le_O_n
- ]
- ]
- |apply (eq_sigma_p_gh ? h h1);intros
- [cut (O < m)
- [cut (i/m < n)
- [cut (i \mod m < m)
- [elim (and_true ? ? H3).
- elim (H ? ? Hcut1 Hcut2 H4 H5).
- elim H6.clear H6.
- elim H8.clear H8.
- elim H6.clear H6.
- elim H8.clear H8.
- cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))/m =
- h11 (i/m) (i\mod m))
- [cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))\mod m =
- h12 (i/m) (i\mod m))
- [rewrite > Hcut3.
- rewrite > Hcut4.
- rewrite > H6.
- rewrite > H12.
- reflexivity
- |apply mod_plus_times.
- assumption
- ]
- |apply div_plus_times.
- assumption
- ]
- |apply lt_mod_m_m.
- assumption
- ]
- |apply (lt_times_n_to_lt m)
- [assumption
- |apply (le_to_lt_to_lt ? i)
- [apply (eq_plus_to_le ? ? (i \mod m)).
- apply div_mod.
- assumption
- |assumption
- ]
- ]
- ]
- |apply not_le_to_lt.unfold.intro.
- generalize in match H2.
- apply (le_n_O_elim ? H4).
- rewrite < times_n_O.
- apply le_to_not_lt.
- apply le_O_n
- ]
- |cut (O < m)
- [cut (i/m < n)
- [cut (i \mod m < m)
- [elim (and_true ? ? H3).
- elim (H ? ? Hcut1 Hcut2 H4 H5).
- elim H6.clear H6.
- elim H8.clear H8.
- elim H6.clear H6.
- elim H8.clear H8.
- cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))/m =
- h11 (i/m) (i\mod m))
- [cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))\mod m =
- h12 (i/m) (i\mod m))
- [rewrite > Hcut3.
- rewrite > Hcut4.
- rewrite > H10.
- rewrite > H11.
- apply sym_eq.
- apply div_mod.
- assumption
- |apply mod_plus_times.
- assumption
- ]
- |apply div_plus_times.
- assumption
- ]
- |apply lt_mod_m_m.
- assumption
- ]
- |apply (lt_times_n_to_lt m)
- [assumption
- |apply (le_to_lt_to_lt ? i)
- [apply (eq_plus_to_le ? ? (i \mod m)).
- apply div_mod.
- assumption
- |assumption
- ]
- ]
- ]
- |apply not_le_to_lt.unfold.intro.
- generalize in match H2.
- apply (le_n_O_elim ? H4).
- rewrite < times_n_O.
- apply le_to_not_lt.
- apply le_O_n
- ]
- |cut (O < m)
- [cut (i/m < n)
- [cut (i \mod m < m)
- [elim (and_true ? ? H3).
- elim (H ? ? Hcut1 Hcut2 H4 H5).
- elim H6.clear H6.
- elim H8.clear H8.
- elim H6.clear H6.
- elim H8.clear H8.
- apply lt_times_plus_times
- [assumption|assumption]
- |apply lt_mod_m_m.
- assumption
- ]
- |apply (lt_times_n_to_lt m)
- [assumption
- |apply (le_to_lt_to_lt ? i)
- [apply (eq_plus_to_le ? ? (i \mod m)).
- apply div_mod.
- assumption
- |assumption
- ]
- ]
- ]
- |apply not_le_to_lt.unfold.intro.
- generalize in match H2.
- apply (le_n_O_elim ? H4).
- rewrite < times_n_O.
- apply le_to_not_lt.
- apply le_O_n
- ]
- |cut (O < m)
- [cut (j/m < n)
- [cut (j \mod m < m)
- [elim (and_true ? ? H3).
- elim (H1 ? ? Hcut1 Hcut2 H4 H5).
- elim H6.clear H6.
- elim H8.clear H8.
- elim H6.clear H6.
- elim H8.clear H8.
- cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))/m =
- h21 (j/m) (j\mod m))
- [cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))\mod m =
- h22 (j/m) (j\mod m))
- [rewrite > Hcut3.
- rewrite > Hcut4.
- rewrite > H6.
- rewrite > H12.
- reflexivity
- |apply mod_plus_times.
- assumption
- ]
- |apply div_plus_times.
- assumption
- ]
- |apply lt_mod_m_m.
- assumption
- ]
- |apply (lt_times_n_to_lt m)
- [assumption
- |apply (le_to_lt_to_lt ? j)
- [apply (eq_plus_to_le ? ? (j \mod m)).
- apply div_mod.
- assumption
- |assumption
- ]
- ]
- ]
- |apply not_le_to_lt.unfold.intro.
- generalize in match H2.
- apply (le_n_O_elim ? H4).
- rewrite < times_n_O.
- apply le_to_not_lt.
- apply le_O_n
- ]
- |cut (O < m)
- [cut (j/m < n)
- [cut (j \mod m < m)
- [elim (and_true ? ? H3).
- elim (H1 ? ? Hcut1 Hcut2 H4 H5).
- elim H6.clear H6.
- elim H8.clear H8.
- elim H6.clear H6.
- elim H8.clear H8.
- cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))/m =
- h21 (j/m) (j\mod m))
- [cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))\mod m =
- h22 (j/m) (j\mod m))
- [rewrite > Hcut3.
- rewrite > Hcut4.
- rewrite > H10.
- rewrite > H11.
- apply sym_eq.
- apply div_mod.
- assumption
- |apply mod_plus_times.
- assumption
- ]
- |apply div_plus_times.
- assumption
- ]
- |apply lt_mod_m_m.
- assumption
- ]
- |apply (lt_times_n_to_lt m)
- [assumption
- |apply (le_to_lt_to_lt ? j)
- [apply (eq_plus_to_le ? ? (j \mod m)).
- apply div_mod.
- assumption
- |assumption
- ]
- ]
- ]
- |apply not_le_to_lt.unfold.intro.
- generalize in match H2.
- apply (le_n_O_elim ? H4).
- rewrite < times_n_O.
- apply le_to_not_lt.
- apply le_O_n
- ]
- |cut (O < m)
- [cut (j/m < n)
- [cut (j \mod m < m)
- [elim (and_true ? ? H3).
- elim (H1 ? ? Hcut1 Hcut2 H4 H5).
- elim H6.clear H6.
- elim H8.clear H8.
- elim H6.clear H6.
- elim H8.clear H8.
- apply (lt_times_plus_times ? ? ? m)
- [assumption|assumption]
- |apply lt_mod_m_m.
- assumption
- ]
- |apply (lt_times_n_to_lt m)
- [assumption
- |apply (le_to_lt_to_lt ? j)
- [apply (eq_plus_to_le ? ? (j \mod m)).
- apply div_mod.
- assumption
- |assumption
- ]
- ]
- ]
- |apply not_le_to_lt.unfold.intro.
- generalize in match H2.
- apply (le_n_O_elim ? H4).
- rewrite < times_n_O.
- apply le_to_not_lt.
- apply le_O_n
- ]
- ]
- ]
-qed.
-
(* dirichlet_product is associative only up to extensional equality *)
theorem associative_dirichlet_product:
\forall f,g,h:nat\to Z.\forall n:nat.O < n \to
(\lambda d,d1:nat.d/d1)
(S n)
(S n)
+ (S n)
+ (S n)
?
?
(\lambda d,d1:nat.divides_b d1 d)
]
qed.
-(* da spostare in times *)
-definition Zone \def pos O.
-
-theorem Ztimes_Zone_l: \forall z:Z. Ztimes Zone z = z.
-intro.unfold Zone.simplify.
-elim z;simplify
- [reflexivity
- |rewrite < plus_n_O.reflexivity
- |rewrite < plus_n_O.reflexivity
- ]
-qed.
-
-theorem Ztimes_Zone_r: \forall z:Z. Ztimes z Zone = z.
-intro.
-rewrite < sym_Ztimes.
-apply Ztimes_Zone_l.
-qed.
-
-theorem injective_Zplus_l: \forall x:Z.injective Z Z (\lambda y.y+x).
-intro.simplify.intros (z y).
-rewrite < Zplus_z_OZ.
-rewrite < (Zplus_z_OZ y).
-rewrite < (Zplus_Zopp x).
-rewrite < (Zplus_Zopp x).
-rewrite < assoc_Zplus.
-rewrite < assoc_Zplus.
-apply eq_f2
- [assumption|reflexivity]
-qed.
-
-theorem injective_Zplus_r: \forall x:Z.injective Z Z (\lambda y.x+y).
-intro.simplify.intros (z y).
-apply (injective_Zplus_l x).
-rewrite < sym_Zplus.
-rewrite > H.
-apply sym_Zplus.
-qed.
-
theorem sigma_p_OZ:
\forall p: nat \to bool.\forall n.sigma_p n p (\lambda m.OZ) = OZ.
intros.elim n
]
qed.
-(* da spostare *)
-theorem notb_notb: \forall b:bool. notb (notb b) = b.
-intros.
-elim b;reflexivity.
-qed.
-
-theorem injective_notb: injective bool bool notb.
-unfold injective.
-intros.
-rewrite < notb_notb.
-rewrite < (notb_notb y).
-apply eq_f.
-assumption.
-qed.
-
-theorem divides_div: \forall d,n. divides d n \to divides (n/d) n.
-intros.
-apply (witness ? ? d).
-apply sym_eq.
-apply divides_to_div.
-assumption.
-qed.
-
-theorem divides_b_div_true:
-\forall d,n. O < n \to
- divides_b d n = true \to divides_b (n/d) n = true.
-intros.
-apply divides_to_divides_b_true1
- [assumption
- |apply divides_div.
- apply divides_b_true_to_divides.
- assumption
- ]
-qed.
-
-(* spostato in primes.ma (non in div_and_mod.ma perche' serve il predicato divides)
-theorem div_div: \forall n,d:nat. O < n \to divides d n \to
-n/(n/d) = d.
-intros.
-apply (inj_times_l1 (n/d))
- [apply (lt_times_n_to_lt d)
- [apply (divides_to_lt_O ? ? H H1).
- |rewrite > divides_to_div;assumption
- ]
- |rewrite > divides_to_div
- [rewrite > sym_times.
- rewrite > divides_to_div
- [reflexivity
- |assumption
- ]
- |apply (witness ? ? d).
- apply sym_eq.
- apply divides_to_div.
- assumption
- ]
- ]
-qed.
-*)
theorem commutative_dirichlet_product: \forall f,g:nat \to Z.\forall n. O < n \to
dirichlet_product f g n = dirichlet_product g f n.
intros.
apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
qed.
+(* transitivity *)
+theorem transitive_Zle : transitive Z Zle.
+unfold transitive.
+intros 3.
+elim x 0
+[ (* x = OZ *)
+ elim y 0
+ [ intros. assumption
+ | intro.
+ elim z
+ [ simplify. apply I
+ | simplify. apply I
+ | simplify. simplify in H1. assumption
+ ]
+ | intro.
+ elim z
+ [ simplify. apply I
+ | simplify. apply I
+ | simplify. simplify in H. assumption
+ ]
+ ]
+| (* x = (pos n) *)
+ intro.
+ elim y 0
+ [ intros. apply False_ind. apply H
+ | intros 2.
+ elim z 0
+ [ simplify. intro. assumption
+ | intro. generalize in match H. simplify. apply trans_le
+ | intro. simplify. intro. assumption
+ ]
+ | intros 2. apply False_ind. apply H
+ ]
+| (* x = (neg n) *)
+ intro.
+ elim y 0
+ [ elim z 0
+ [ simplify. intros. assumption
+ | intro. simplify. intros. assumption
+ | intro. simplify. intros. apply False_ind. apply H1
+ ]
+ | intros 2.
+ elim z
+ [ apply False_ind. apply H1
+ | simplify. apply I
+ | apply False_ind. apply H1
+ ]
+ | intros 2.
+ elim z 0
+ [ simplify. intro. assumption
+ | intro. simplify. intro. assumption
+ | intros. simplify. simplify in H. simplify in H1.
+ generalize in match H. generalize in match H1. apply trans_le
+ ]
+ ]
+]
+qed.
+
+variant trans_Zle: transitive Z Zle
+\def transitive_Zle.
+
+theorem transitive_Zlt: transitive Z Zlt.
+unfold.
+intros 3.
+elim x 0
+[ (* x = OZ *)
+ elim y 0
+ [ intros. apply False_ind. apply H
+ | intro.
+ elim z
+ [ simplify. apply H1
+ | simplify. apply I
+ | simplify. apply H1
+ ]
+ | intros 2. apply False_ind. apply H
+ ]
+| (* x = (pos n) *)
+ intro.
+ elim y 0
+ [ intros. apply False_ind. apply H
+ | intros 2.
+ elim z 0
+ [ simplify. intro. assumption
+ | intro. generalize in match H. simplify. apply trans_lt
+ | intro. simplify. intro. assumption
+ ]
+ | intros 2. apply False_ind. apply H
+ ]
+| (* x = (neg n) *)
+ intro.
+ elim y 0
+ [ elim z 0
+ [ intros. simplify. apply I
+ | intro. simplify. intros. assumption
+ | intro. simplify. intros. apply False_ind. apply H1
+ ]
+ | intros 2.
+ elim z
+ [ apply False_ind. apply H1
+ | simplify. apply I
+ | apply False_ind. apply H1
+ ]
+ | intros 2.
+ elim z 0
+ [ simplify. intro. assumption
+ | intro. simplify. intro. assumption
+ | intros. simplify. simplify in H. simplify in H1.
+ generalize in match H. generalize in match H1. apply trans_lt
+ ]
+ ]
+]
+qed.
+
+variant trans_Zlt: transitive Z Zlt
+\def transitive_Zlt.
theorem irrefl_Zlt: irreflexive Z Zlt
\def irreflexive_Zlt.
|intros.apply sym_Ztimes
]
qed.
+
+
+(* sigma from n1*m1 to n2*m2 *)
+theorem sigma_p2_eq:
+\forall g: nat \to nat \to Z.
+\forall h11,h12,h21,h22: nat \to nat \to nat.
+\forall n1,m1,n2,m2.
+\forall p11,p21:nat \to bool.
+\forall p12,p22:nat \to nat \to bool.
+(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
+p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
+\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
+\land h11 i j < n1 \land h12 i j < m1) \to
+(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
+p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
+\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
+\land (h21 i j) < n2 \land (h22 i j) < m2) \to
+sigma_p n1 p11 (\lambda x:nat .sigma_p m1 (p12 x) (\lambda y. g x y)) =
+sigma_p n2 p21 (\lambda x:nat .sigma_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
+intros.
+rewrite < sigma_p2'.
+rewrite < sigma_p2'.
+apply sym_eq.
+letin h := (\lambda x.(h11 (x/m2) (x\mod m2))*m1 + (h12 (x/m2) (x\mod m2))).
+letin h1 := (\lambda x.(h21 (x/m1) (x\mod m1))*m2 + (h22 (x/m1) (x\mod m1))).
+apply (trans_eq ? ?
+ (sigma_p (n2*m2) (\lambda x:nat.p21 (x/m2)\land p22 (x/m2) (x\mod m2))
+ (\lambda x:nat.g ((h x)/m1) ((h x)\mod m1))))
+ [clear h.clear h1.
+ apply eq_sigma_p1
+ [intros.reflexivity
+ |intros.
+ cut (O < m2)
+ [cut (x/m2 < n2)
+ [cut (x \mod m2 < m2)
+ [elim (and_true ? ? H3).
+ elim (H ? ? Hcut1 Hcut2 H4 H5).
+ elim H6.clear H6.
+ elim H8.clear H8.
+ elim H6.clear H6.
+ elim H8.clear H8.
+ apply eq_f2
+ [apply sym_eq.
+ apply div_plus_times.
+ assumption
+ |autobatch
+ ]
+ |apply lt_mod_m_m.
+ assumption
+ ]
+ |apply (lt_times_n_to_lt m2)
+ [assumption
+ |apply (le_to_lt_to_lt ? x)
+ [apply (eq_plus_to_le ? ? (x \mod m2)).
+ apply div_mod.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |apply not_le_to_lt.unfold.intro.
+ generalize in match H2.
+ apply (le_n_O_elim ? H4).
+ rewrite < times_n_O.
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ ]
+ |apply (eq_sigma_p_gh ? h h1);intros
+ [cut (O < m2)
+ [cut (i/m2 < n2)
+ [cut (i \mod m2 < m2)
+ [elim (and_true ? ? H3).
+ elim (H ? ? Hcut1 Hcut2 H4 H5).
+ elim H6.clear H6.
+ elim H8.clear H8.
+ elim H6.clear H6.
+ elim H8.clear H8.
+ cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 =
+ h11 (i/m2) (i\mod m2))
+ [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
+ h12 (i/m2) (i\mod m2))
+ [rewrite > Hcut3.
+ rewrite > Hcut4.
+ rewrite > H6.
+ rewrite > H12.
+ reflexivity
+ |apply mod_plus_times.
+ assumption
+ ]
+ |apply div_plus_times.
+ assumption
+ ]
+ |apply lt_mod_m_m.
+ assumption
+ ]
+ |apply (lt_times_n_to_lt m2)
+ [assumption
+ |apply (le_to_lt_to_lt ? i)
+ [apply (eq_plus_to_le ? ? (i \mod m2)).
+ apply div_mod.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |apply not_le_to_lt.unfold.intro.
+ generalize in match H2.
+ apply (le_n_O_elim ? H4).
+ rewrite < times_n_O.
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ |cut (O < m2)
+ [cut (i/m2 < n2)
+ [cut (i \mod m2 < m2)
+ [elim (and_true ? ? H3).
+ elim (H ? ? Hcut1 Hcut2 H4 H5).
+ elim H6.clear H6.
+ elim H8.clear H8.
+ elim H6.clear H6.
+ elim H8.clear H8.
+ cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 =
+ h11 (i/m2) (i\mod m2))
+ [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
+ h12 (i/m2) (i\mod m2))
+ [rewrite > Hcut3.
+ rewrite > Hcut4.
+ rewrite > H10.
+ rewrite > H11.
+ apply sym_eq.
+ apply div_mod.
+ assumption
+ |apply mod_plus_times.
+ assumption
+ ]
+ |apply div_plus_times.
+ assumption
+ ]
+ |apply lt_mod_m_m.
+ assumption
+ ]
+ |apply (lt_times_n_to_lt m2)
+ [assumption
+ |apply (le_to_lt_to_lt ? i)
+ [apply (eq_plus_to_le ? ? (i \mod m2)).
+ apply div_mod.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |apply not_le_to_lt.unfold.intro.
+ generalize in match H2.
+ apply (le_n_O_elim ? H4).
+ rewrite < times_n_O.
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ |cut (O < m2)
+ [cut (i/m2 < n2)
+ [cut (i \mod m2 < m2)
+ [elim (and_true ? ? H3).
+ elim (H ? ? Hcut1 Hcut2 H4 H5).
+ elim H6.clear H6.
+ elim H8.clear H8.
+ elim H6.clear H6.
+ elim H8.clear H8.
+ apply lt_times_plus_times
+ [assumption|assumption]
+ |apply lt_mod_m_m.
+ assumption
+ ]
+ |apply (lt_times_n_to_lt m2)
+ [assumption
+ |apply (le_to_lt_to_lt ? i)
+ [apply (eq_plus_to_le ? ? (i \mod m2)).
+ apply div_mod.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |apply not_le_to_lt.unfold.intro.
+ generalize in match H2.
+ apply (le_n_O_elim ? H4).
+ rewrite < times_n_O.
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ |cut (O < m1)
+ [cut (j/m1 < n1)
+ [cut (j \mod m1 < m1)
+ [elim (and_true ? ? H3).
+ elim (H1 ? ? Hcut1 Hcut2 H4 H5).
+ elim H6.clear H6.
+ elim H8.clear H8.
+ elim H6.clear H6.
+ elim H8.clear H8.
+ cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 =
+ h21 (j/m1) (j\mod m1))
+ [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
+ h22 (j/m1) (j\mod m1))
+ [rewrite > Hcut3.
+ rewrite > Hcut4.
+ rewrite > H6.
+ rewrite > H12.
+ reflexivity
+ |apply mod_plus_times.
+ assumption
+ ]
+ |apply div_plus_times.
+ assumption
+ ]
+ |apply lt_mod_m_m.
+ assumption
+ ]
+ |apply (lt_times_n_to_lt m1)
+ [assumption
+ |apply (le_to_lt_to_lt ? j)
+ [apply (eq_plus_to_le ? ? (j \mod m1)).
+ apply div_mod.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |apply not_le_to_lt.unfold.intro.
+ generalize in match H2.
+ apply (le_n_O_elim ? H4).
+ rewrite < times_n_O.
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ |cut (O < m1)
+ [cut (j/m1 < n1)
+ [cut (j \mod m1 < m1)
+ [elim (and_true ? ? H3).
+ elim (H1 ? ? Hcut1 Hcut2 H4 H5).
+ elim H6.clear H6.
+ elim H8.clear H8.
+ elim H6.clear H6.
+ elim H8.clear H8.
+ cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 =
+ h21 (j/m1) (j\mod m1))
+ [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
+ h22 (j/m1) (j\mod m1))
+ [rewrite > Hcut3.
+ rewrite > Hcut4.
+ rewrite > H10.
+ rewrite > H11.
+ apply sym_eq.
+ apply div_mod.
+ assumption
+ |apply mod_plus_times.
+ assumption
+ ]
+ |apply div_plus_times.
+ assumption
+ ]
+ |apply lt_mod_m_m.
+ assumption
+ ]
+ |apply (lt_times_n_to_lt m1)
+ [assumption
+ |apply (le_to_lt_to_lt ? j)
+ [apply (eq_plus_to_le ? ? (j \mod m1)).
+ apply div_mod.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |apply not_le_to_lt.unfold.intro.
+ generalize in match H2.
+ apply (le_n_O_elim ? H4).
+ rewrite < times_n_O.
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ |cut (O < m1)
+ [cut (j/m1 < n1)
+ [cut (j \mod m1 < m1)
+ [elim (and_true ? ? H3).
+ elim (H1 ? ? Hcut1 Hcut2 H4 H5).
+ elim H6.clear H6.
+ elim H8.clear H8.
+ elim H6.clear H6.
+ elim H8.clear H8.
+ apply (lt_times_plus_times ? ? ? m2)
+ [assumption|assumption]
+ |apply lt_mod_m_m.
+ assumption
+ ]
+ |apply (lt_times_n_to_lt m1)
+ [assumption
+ |apply (le_to_lt_to_lt ? j)
+ [apply (eq_plus_to_le ? ? (j \mod m1)).
+ apply div_mod.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |apply not_le_to_lt.unfold.intro.
+ generalize in match H2.
+ apply (le_n_O_elim ? H4).
+ rewrite < times_n_O.
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ ]
+ ]
+qed.
\ No newline at end of file
projects / helm.git / commitdiff