(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) (* This includes a lot of copied code from arithmetics/Z.ma, so some of the comments may no longer be applicable. *) (*include "arithmetics/compare.ma".*) include "utilities/binary/positive.ma". inductive Z : Type[0] ≝ OZ : Z | pos : Pos → Z | neg : Pos → Z. (*interpretation "Integers" 'D = Z.*) definition Z_of_nat ≝ λn. match n with [ O ⇒ OZ | S n ⇒ pos (succ_pos_of_nat n)]. coercion Z_of_nat : ∀n:nat.Z ≝ Z_of_nat on _n:nat to Z. definition neg_Z_of_nat \def λn. match n with [ O ⇒ OZ | S n ⇒ neg (succ_pos_of_nat n)]. definition abs ≝ λz.match z with [ OZ ⇒ O | pos n ⇒ nat_of_pos n | neg n ⇒ nat_of_pos n]. definition OZ_test ≝ λz.match z with [ OZ ⇒ true | pos _ ⇒ false | neg _ ⇒ false]. theorem OZ_test_to_Prop : ∀z:Z. match OZ_test z with [true ⇒ z=OZ |false ⇒ z ≠ OZ]. #z cases z [ @refl |*:#z1 @nmk #H destruct] qed. (* discrimination *) theorem injective_pos: injective Pos Z pos. #n #m #H destruct // qed. (* variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m \def injective_pos. *) theorem injective_neg: injective Pos Z neg. #n #m #H destruct // qed. (* variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m \def injective_neg. *) theorem not_eq_OZ_pos: ∀n:Pos. OZ ≠ pos n. #n @nmk #H destruct; qed. theorem not_eq_OZ_neg :∀n:Pos. OZ ≠ neg n. #n @nmk #H destruct; qed. theorem not_eq_pos_neg : ∀n,m:Pos. pos n ≠ neg m. #n #m @nmk #H destruct; qed. theorem decidable_eq_Z : ∀x,y:Z. decidable (x=y). #x #y cases x; [cases y; [% // |*:#n %2 @nmk #H destruct] |#n cases y; [%2 @nmk #H destruct; |#m cases (decidable_eq_pos n m) #H [>H % // |%2 @(not_to_not … H) #E destruct @refl ] |#m %2 @nmk #H destruct] |#n cases y; [%2 @nmk #H destruct; |#m %2 @nmk #H destruct |#m cases (decidable_eq_pos n m);#H [>H % // |%2 @(not_to_not … H) #E destruct @refl ]]] qed. definition Zsucc ≝ λz. match z with [ OZ ⇒ pos one | pos n ⇒ pos (succ n) | neg n ⇒ match n with [ one ⇒ OZ | _ ⇒ neg (pred n)]]. definition Zpred ≝ λz. match z with [ OZ ⇒ neg one | pos n ⇒ match n with [ one ⇒ OZ | _ ⇒ pos (pred n)] | neg n ⇒ neg (succ n)]. lemma pred_succ_unfold_hack: ∀p. Zpred (Zsucc (neg (p0 p))) = neg (succ (pred (p0 p))). //; qed. theorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z. #z cases z; [ // | #n normalize; cases n; /2/; | #n cases n; //; #n' >(pred_succ_unfold_hack …) <(succ_pred_n …) //; % #H destruct; qed. lemma succ_pred_unfold_hack: ∀p. Zsucc (Zpred (pos (p0 p))) = pos (succ (pred (p0 p))). //; qed. theorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z. #z cases z [ // | #n cases n;//; #n' >(succ_pred_unfold_hack …) <(succ_pred_n …) //; % #H destruct; | #n cases n;/3/; ] qed. let rec Zle (x:Z) (y:Z) on x : Prop ≝ match x with [ OZ ⇒ match y with [ OZ ⇒ True | pos m ⇒ True | neg m ⇒ False ] | pos n ⇒ match y with [ OZ ⇒ False | pos m ⇒ n ≤ m | neg m ⇒ False ] | neg n ⇒ match y with [ OZ ⇒ True | pos m ⇒ True | neg m ⇒ m ≤ n ]]. interpretation "integer 'less or equal to'" 'leq x y = (Zle x y). interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)). let rec Zlt (x:Z) (y:Z) on x : Prop ≝ match x with [ OZ ⇒ match y with [ OZ ⇒ False | pos m ⇒ True | neg m ⇒ False ] | pos n ⇒ match y with [ OZ ⇒ False | pos m ⇒ n(Zsucc_neg_succ m) @le_S_S_to_le (* XXX: auto? *) ] ] ] qed. (*** COMPARE ***) (* boolean equality *) let rec eqZb (x:Z) (y:Z) on x : bool ≝ match x with [ OZ ⇒ match y with [ OZ ⇒ true | pos q ⇒ false | neg q ⇒ false] | pos p ⇒ match y with [ OZ ⇒ false | pos q ⇒ eqb p q | neg q ⇒ false] | neg p ⇒ match y with [ OZ ⇒ false | pos q ⇒ false | neg q ⇒ eqb p q]]. theorem eqZb_to_Prop: ∀x,y:Z. match eqZb x y with [ true ⇒ x=y | false ⇒ x ≠ y]. #x #y cases x [cases y; [// |@not_eq_OZ_pos (* XXX: auto? *) |@not_eq_OZ_neg (* XXX: auto? *)] |#n cases y; [@nmk #H elim (not_eq_OZ_pos n);#H2 /2/; |#m normalize @eqb_elim [// | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) // ] |#m @not_eq_pos_neg] |#n cases y [@nmk #H elim (not_eq_OZ_neg n);#H /2/; |#m @nmk #H destruct |#m normalize @eqb_elim [// | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) // ] ] qed. theorem eqZb_elim: ∀x,y:Z.∀P:bool → Prop. (x=y → P true) → (x ≠ y → P false) → P (eqZb x y). #x #y #P #HP1 #HP2 cut (match (eqZb x y) with [ true ⇒ x=y | false ⇒ x ≠ y] → P (eqZb x y)) [cases (eqZb x y);normalize; (* XXX: auto?? *) [@HP1 |@HP2] |#Hcut @Hcut @eqZb_to_Prop] qed. let rec Z_compare (x:Z) (y:Z) : compare ≝ match x with [ OZ ⇒ match y with [ OZ ⇒ EQ | pos m ⇒ LT | neg m ⇒ GT ] | pos n ⇒ match y with [ OZ ⇒ GT | pos m ⇒ pos_compare n m | neg m ⇒ GT] | neg n ⇒ match y with [ OZ ⇒ LT | pos m ⇒ LT | neg m ⇒ pos_compare m n ]]. theorem Z_compare_to_Prop : ∀x,y:Z. match (Z_compare x y) with [ LT ⇒ x < y | EQ ⇒ x=y | GT ⇒ y < x]. #x #y elim x [elim y;//; |elim y [1,3:// |#n #m normalize; cut (match (pos_compare m n) with [ LT ⇒ m < n | EQ ⇒ m = n | GT ⇒ n < m ] → match (pos_compare m n) with [ LT ⇒ (succ m) ≤ n | EQ ⇒ pos m = pos n | GT ⇒ (succ n) ≤ m]) [cases (pos_compare m n);// |#Hcut @Hcut @pos_compare_to_Prop] ] |elim y [#n // |normalize;// |normalize;#n #m cut (match (pos_compare n m) with [ LT ⇒ n < m | EQ ⇒ n = m | GT ⇒ m < n] → match (pos_compare n m) with [ LT ⇒ (succ n) ≤ m | EQ ⇒ neg m = neg n | GT ⇒ (succ m) ≤ n]) [cases (pos_compare n m);// |#Hcut @Hcut @pos_compare_to_Prop] ] ] qed. let rec Zplus (x:Z) (y:Z) on x : Z ≝ match x with [ OZ ⇒ y | pos m ⇒ match y with [ OZ ⇒ x | pos n ⇒ (pos (m + n)) | neg n ⇒ match pos_compare m n with [ LT ⇒ (neg (n-m)) | EQ ⇒ OZ | GT ⇒ (pos (m-n))] ] | neg m ⇒ match y with [ OZ ⇒ x | pos n ⇒ match pos_compare m n with [ LT ⇒ (pos (n-m)) | EQ ⇒ OZ | GT ⇒ (neg (m-n))] | neg n ⇒ (neg (m + n))] ]. interpretation "integer plus" 'plus x y = (Zplus x y). theorem eq_plus_Zplus: ∀n,m:nat. Z_of_nat (n+m) = Z_of_nat n + Z_of_nat m. #n #m cases n [// |#p cases m [normalize;// |#m' normalize;>(nat_plus_pos_plus …) >(succ_nat_pos ?) /2/] qed. theorem eq_pplus_Zplus: ∀n,m:Pos. pos (n+m) = pos n + pos m. //; qed. theorem Zplus_z_OZ: ∀z:Z. z+OZ = z. #z cases z;//; qed. theorem sym_Zplus : ∀x,y:Z. x+y = y+x. #x #y cases x [>Zplus_z_OZ // |#p cases y [// |// |#q whd in ⊢ (??%%); >pos_compare_n_m_m_n cases (pos_compare q p);//] |#p cases y [//; |#q whd in ⊢ (??%%); >pos_compare_n_m_m_n cases (pos_compare q p);// |normalize;//] ] qed. theorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg one)+z. #z cases z [// |*:#n cases n;//] qed. theorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos one)+z. #z cases z [// |*:#n cases n;//] qed. lemma Zpred_pos_succ: ∀n. Zpred (pos (succ n)) = pos n. #n normalize; cases n; /2/; qed. theorem Zplus_pos_pos: ∀n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)). #n #m @(pos_cases … n) [ @(pos_cases … m) //; |#p @(pos_cases … m) [normalize; <(succ_plus_one …) //; |#q >(Zsucc_Zplus_pos_O …) >(Zpred_pos_succ ?) normalize; /2/; ] ] qed. theorem Zplus_pos_neg: ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)). #n #m whd in ⊢ (??%%); <(pos_compare_S_S …) >(minus_S_S …) >(minus_S_S …) //; qed. lemma pos_nonzero: ∀A.∀P:Pos→A.∀Q,n. match succ n with [ one ⇒ Q | p0 p ⇒ P n | p1 p ⇒ P n ] = P n. #A #P #Q #n @succ_elim //; qed. lemma partial_minus_S_one: ∀n. partial_minus (succ n) one = MinusPos n. #n cases n; //; #n' whd in ⊢ (??%?); normalize; <(pred_succ_n …) @succ_elim //; qed. theorem Zplus_neg_pos : ∀n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)). #n #m @(pos_cases … n) @(pos_cases … m) [ //; | #m' >Zpred_pos_succ change with (Zsucc (pos m')) in ⊢ (??(??%)?); Zpred_Zsucc @refl | #m' whd in ⊢ (??%%); >pos_compare_S_one normalize; >partial_minus_S_one normalize; >pos_nonzero minus_S_S >minus_S_S normalize >pos_nonzero >pos_nonzero (pos_nonzero …) <(pred_succ_n …) normalize; //; | #m' #n' normalize; >(pos_nonzero …) <(pred_succ_n …) normalize; //; ] qed. theorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y). #x #y cases x [cases y [// |#n <(Zsucc_Zplus_pos_O ?) >(Zsucc_Zpred ?) // |#p <(Zsucc_Zplus_pos_O …) //] |cases y;/2/; #p >(sym_Zplus ? (Zpred OZ)) (Zpred_Zsucc ?) // |*:/2/] qed. theorem Zplus_Zsucc_pos_pos : ∀n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)). #n #m >(Zsucc_Zplus_pos_O ?) >(Zsucc_Zplus_pos_O ?) //; qed. theorem Zplus_Zsucc_pos_neg: ∀n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))). #n #m @(pos_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))))) [#n1 elim n1 [// |*:#n2 #IH elim n2;//] |#n' >(sym_Zplus …) <(Zpred_Zplus_neg_O ?) >(sym_Zplus …) <(Zpred_Zplus_neg_O ?) >(Zpred_Zsucc …) /2/ |#n1 #m1 #IH <(Zplus_pos_neg ? m1) >IH <(Zplus_pos_neg …) //] qed. theorem Zplus_Zsucc_neg_neg : ∀n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m). #n #m @(pos_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m))) [@pos_elim [// |#n2 #IH normalize;<(pred_succ_n …) >(pos_nonzero …) //] | #n' normalize; >(pos_nonzero …) <(pred_succ_n …) normalize; <(succ_plus_one …) <(succ_plus_one …) >(pos_nonzero …) //; | #n' #m' #IH normalize; >(pos_nonzero …) normalize; <(pluss_succn_m …) >(pos_nonzero …) //; ] qed. lemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m. #n #m whd in ⊢ (??%%); minus_S_S >minus_S_S //; qed. theorem Zplus_Zsucc_neg_pos: ∀n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)). #n #m @(pos_elim2 (λn,m. (Zsucc (neg n)) + (pos m) = Zsucc (neg n + pos m))) [@pos_elim [// |#n2 #IH normalize; >(pos_nonzero …) normalize; >(partial_minus_S_one …) //] | #n' >(sym_Zplus …) <(Zsucc_Zplus_pos_O …) >(sym_Zplus …) <(Zsucc_Zplus_pos_O …) //; |#n' #m' #IH >(neg_pos_succ …) //; ] qed. theorem Zplus_Zsucc : ∀x,y:Z. (Zsucc x)+y = Zsucc (x+y). #x #y cases x [cases y;//;(*#n normalize;cases n;//;*) |*:#n cases y;//;#m @Zplus_Zsucc_neg_pos(* XXX: // didn't work! *)] qed. theorem Zplus_Zpred: ∀x,y:Z. (Zpred x)+y = Zpred (x+y). #x #y cut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y)) [>(Zsucc_Zpred ?) // |#Hcut >Hcut >(Zplus_Zsucc ??) //] qed. theorem associative_Zplus: associative Z Zplus. (* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*) #x #y #z cases x [// |@pos_elim [<(Zsucc_Zplus_pos_O ?) <(Zsucc_Zplus_pos_O ?) //; |#n1 #IH >(Zplus_Zsucc (pos n1) ?) >(Zplus_Zsucc (pos n1) ?) >(Zplus_Zsucc ((pos n1)+y) ?) //] |@pos_elim [<(Zpred_Zplus_neg_O (y+z)) <(Zpred_Zplus_neg_O y) //; |#n1 #IH >(Zplus_Zpred (neg n1) ?) >(Zplus_Zpred (neg n1) ?) >(Zplus_Zpred ((neg n1)+y) ?) //] ] qed. (* variant assoc_Zplus : \forall x,y,z:Z. (x+y)+z = x+(y+z) \def associative_Zplus. *) (* Zopp *) definition Zopp : Z → Z ≝ λx:Z. match x with [ OZ ⇒ OZ | pos n ⇒ neg n | neg n ⇒ pos n ]. interpretation "integer unary minus" 'uminus x = (Zopp x). theorem eq_OZ_Zopp_OZ : OZ = (- OZ). //; qed. theorem Zopp_Zplus: ∀x,y:Z. -(x+y) = -x + -y. #x #y cases x [cases y;// |*:#n cases y;//;#m whd in ⊢ (??(?%)%); @pos_compare_elim normalize;//] qed. theorem Zopp_Zopp: ∀x:Z. --x = x. #x cases x;//; qed. theorem Zplus_Zopp: ∀ x:Z. x+ -x = OZ. #x cases x [// |*:#n whd in ⊢ (??%?); >pos_compare_n_n //] qed. theorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x). #x #z #y #H <(Zplus_z_OZ z) <(Zplus_z_OZ y) <(Zplus_Zopp x) <(associative_Zplus ???) <(associative_Zplus ???) //; qed. theorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y). #x #z #y #H @(injective_Zplus_l x) <(sym_Zplus ??) //; qed. (* minus *) definition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y). interpretation "integer minus" 'minus x y = (Zminus x y). definition Z_two_power_nat : nat → Z ≝ λn. pos (two_power_nat n). definition Z_two_power_pos : Pos → Z ≝ λn. pos (two_power_pos n). definition two_p : Z → Z ≝ λz.match z with [ OZ ⇒ pos one | pos p ⇒ pos (two_power_pos p) | neg _ ⇒ OZ (* same fib as Coq *) ]. lemma eqZb_z_z : ∀z.eqZb z z = true. #z cases z;normalize;//; qed. lemma injective_Z_of_nat : injective ? ? Z_of_nat. normalize; #n #m cases n;cases m;normalize;//; [ 1,2: #n' #H destruct | #n' #m' #H destruct; >(succ_pos_of_nat_inj … e0) // ] qed. lemma reflexive_Zle : reflexive ? Zle. #x cases x; //; qed. lemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n). #n cases n;normalize;//;qed. lemma Zsucc_le : ∀x:Z. x ≤ Zsucc x. #x cases x; //; #n cases n; //; qed. lemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n. #x #y @pos_elim [ 2: #n' #IH ] >(Zplus_Zsucc_Zpred y ?) [ >(Zpred_Zsucc (pos n')) #H @(transitive_Zle ??? (IH H)) >(Zplus_Zsucc ??) @Zsucc_le | #H @(transitive_Zle ??? H) >(Zplus_z_OZ ?) @Zsucc_le ] qed. theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y. #x #y cases x; [ cases y; [ 1,2: // | #n @False_ind ] | #n cases y; [ normalize; @False_ind | #m @(pos_cases … n) /2/; | #m normalize; @False_ind ] | #n cases y; /2/; ] qed. theorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p. #n #m #p #Hlt #Hle <(Zpred_Zsucc n) @Zle_to_Zlt @(transitive_Zle … Hle) /2/; qed. include "basics/types.ma". definition decidable_eq_Z_Type : ∀z1,z2:Z. (z1 = z2) + (z1 ≠ z2). #z1 #z2 lapply (eqZb_to_Prop z1 z2);cases (eqZb z1 z2);normalize;#H [% // |%2 //] qed. lemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false. #z1 #z2 lapply (eqZb_to_Prop z1 z2); cases (eqZb z1 z2); //; #H #H' @False_ind @(absurd ? H H') qed. (* Z.ma *) definition Zge: Z → Z → Prop ≝ λn,m:Z.m ≤ n. interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y). definition Zgt: Z → Z → Prop ≝ λn,m:Z.m(Zle_to_Zleb_true … H') in H; #H destruct; qed. theorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true. #n #m cases n;cases m; //; [ normalize; #H @(False_ind ? H) | 2,3: #m' normalize; #H @(False_ind ? H) | 4,6: #n' #m' normalize; @le_to_leb_true | #n' #m' normalize; #H @(False_ind ? H) ] qed. theorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m. #n #m cases n;cases m; //; [ normalize; #H destruct | 2,3: #m' normalize; #H destruct | 4,6: #n' #m' @leb_true_to_le | #n' #m' normalize; #H destruct ] qed. theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m. #n #m #H % #H' >(Zlt_to_Zltb_true … H') in H; #H destruct; qed. theorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. (n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m). #n #m #P #Hle #Hnle lapply (refl ? (Zleb n m)); elim (Zleb n m) in ⊢ ((???%)→%); #Hb [ @Hle @(Zleb_true_to_Zle … Hb) | @Hnle @(Zleb_false_to_not_Zle … Hb) ] qed. theorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. (n < m → P true) → (n ≮ m → P false) → P (Zltb n m). #n #m #P #Hlt #Hnlt lapply (refl ? (Zltb n m)); elim (Zltb n m) in ⊢ ((???%)→%); #Hb [ @Hlt @(Zltb_true_to_Zlt … Hb) | @Hnlt @(Zltb_false_to_not_Zlt … Hb) ] qed. lemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc. #x #y cases x; cases y; /2/; #n #m @(pos_cases … n) @(pos_cases … m) [ //; | #n' /2/; | #m' #H @False_ind normalize in H; @(absurd … (not_le_succ_one m')) /2/; | #n' #m' #H normalize in H; >(Zsucc_neg_succ n') >(Zsucc_neg_succ m') /2/; ] qed. lemma monotonic_Zle_Zpred: monotonic Z Zle Zpred. #x #y cases x; cases y; [ 1,2,7,8,9: /2/; | 3,4: #m normalize; *; | #m #n @(pos_cases … n) @(pos_cases … m) [ 1,2: /2/; | #n' normalize; #H @False_ind @(absurd … (not_le_succ_one n')) /2/; | #n' #m' >(Zpred_pos_succ n') >(Zpred_pos_succ m') /2/; ] | #m #n normalize; *; ] qed. lemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m). #n cases n; //; #n' #a #b #H [ @(pos_elim … n') [ <(Zsucc_Zplus_pos_O a) <(Zsucc_Zplus_pos_O b) /2/; | #n'' #H >(?:pos (succ n'') = Zsucc (pos n'')) //; >(Zplus_Zsucc …) >(Zplus_Zsucc …) /2/; ] | @(pos_elim … n') [ <(Zpred_Zplus_neg_O a) <(Zpred_Zplus_neg_O b) /2/; | #n'' #H >(?:neg (succ n'') = Zpred (neg n'')) //; >(Zplus_Zpred …) >(Zplus_Zpred …) /2/; ] ] qed. lemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n). /2/; qed. let rec Z_times (x:Z) (y:Z) : Z ≝ match x with [ OZ ⇒ OZ | pos n ⇒ match y with [ OZ ⇒ OZ | pos m ⇒ pos (n*m) | neg m ⇒ neg (n*m) ] | neg n ⇒ match y with [ OZ ⇒ OZ | pos m ⇒ neg (n*m) | neg m ⇒ pos (n*m) ] ]. interpretation "integer multiplication" 'times x y = (Z_times x y). definition Zmax : Z → Z → Z ≝ λx,y.match Z_compare x y with [ LT ⇒ y | _ ⇒ x ]. lemma Zmax_l: ∀x,y. x ≤ Zmax x y. #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y) /3/ qed. lemma Zmax_r: ∀x,y. y ≤ Zmax x y. #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y) whd in ⊢ (% → ??%); /3/ qed. lemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x. #x #y cases y; [ #H @(False_ind … H) | #m #_ cases x; //; #n whd in ⊢ (?%?); lapply (pos_compare_to_Prop n m); cases (pos_compare n m); /2/ #lt whd <(minus_Sn_m … lt) /2/; | #m #H @(False_ind … H) ] qed.