source: src/utilities/binary/positive.ma @ 1528

Last change on this file since 1528 was 1528, checked in by campbell, 8 years ago

Update most of Assembly.ma with new syntax and identifier maps.
Change positive.ma a little to reduce name clashes.

File size: 29.5 KB
RevLine 
[10]1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15(* little endian positive binary numbers. *)
16
[487]17include "basics/logic.ma".
[10]18include "arithmetics/nat.ma".
19
[487]20(* arithmetics/comparison.ma --> *)
21inductive compare : Type[0] ≝
22| LT : compare
23| EQ : compare
24| GT : compare.
25
26definition compare_invert: compare → compare ≝
27  λc.match c with
28      [ LT ⇒ GT
29      | EQ ⇒ EQ
30      | GT ⇒ LT ].
31
32(* <-- *)
33
34inductive Pos : Type[0] ≝
[10]35  | one : Pos
36  |  p1 : Pos → Pos
37  |  p0 : Pos → Pos.
38
[487]39let rec pred (n:Pos) ≝
[10]40  match n with
41  [ one ⇒ one
42  | p1 ps ⇒ p0 ps
43  | p0 ps ⇒ match ps with [ one ⇒ one | _ ⇒ p1 (pred ps) ]
44  ].
45
[487]46example test : pred (p0 (p0 (p0 one))) = p1 (p1 one).
47//; qed.
[10]48
[487]49let rec succ (n:Pos) ≝
[10]50  match n with
51  [ one ⇒ p0 one
52  | p0 ps ⇒ p1 ps
53  | p1 ps ⇒ p0 (succ ps)
54  ].
55
[487]56lemma succ_elim : ∀P:Pos → Prop. (∀n. P (p0 n)) → (∀n. P (p1 n)) → ∀n. P (succ n).
57#P #H0 #H1 #n cases n; normalize; //; qed.
[10]58
[487]59theorem pred_succ_n : ∀n. n = pred (succ n).
60#n elim n;
61[ 1,3: //
62| #p' normalize; @succ_elim /2/;
63] qed.
[10]64(*
[487]65theorem succ_pred_n : ∀n. n≠one → n = succ (pred n).
66#n elim n;
67[ #H @False_ind elim H; /2/;
68| //;
69| #n' cases n'; /2/; #n'' #IH #_ <IH normalize; 
[10]70*)
[487]71theorem succ_injective: injective Pos Pos succ.
72//; qed.
[10]73
[487]74let rec nat_of_pos (p:Pos) : nat ≝
[10]75  match p with
76  [ one ⇒ 1
77  | p0 ps ⇒ 2 * (nat_of_pos ps)
78  | p1 ps ⇒ S (2 * (nat_of_pos ps))
79  ].
80
[487]81let rec succ_pos_of_nat (n:nat) : Pos ≝
[10]82  match n with
83  [ O ⇒ one
84  | S n' ⇒ succ (succ_pos_of_nat n')
85  ].
86
[487]87theorem succ_nat_pos: ∀n:nat. succ_pos_of_nat (S n) = succ (succ_pos_of_nat n).
88//; qed.
[10]89
[487]90theorem succ_pos_of_nat_inj: injective ?? succ_pos_of_nat.
91#n elim n;
92[ #m cases m;
93  [ //
94  | #m' normalize; @succ_elim #p #H destruct
95  ]
96| #n' #IH #m cases m;
97  [ normalize; @succ_elim #p #H destruct;
98  | normalize; #m' #H >(IH m' ?) //;
99  ]
100] qed.
[10]101
[487]102example test2 : nat_of_pos (p0 (p1 one)) = 6. //; qed.
[10]103
104(* Usual induction principle; proof roughly following Coq's,
105   apparently due to Conor McBride. *)
106
[487]107inductive possucc : Pos → Prop ≝
[10]108  | psone  : possucc one
109  | pssucc : ∀n. possucc n → possucc (succ n).
110
[487]111let rec possucc0 (n:Pos) (p:possucc n) on p : possucc (p0 n) ≝
[10]112  match p return λn',p'.possucc (p0 n') with
113  [ psone ⇒ pssucc ? psone
114  | pssucc _ p'' ⇒ pssucc ? (pssucc ? (possucc0 ? p''))
115  ].
116
[487]117let rec possucc1 (n:Pos) (p:possucc n) on p : possucc (p1 n) ≝
[10]118  match p return λn',p'. possucc (p1 n') with
119  [ psone ⇒ pssucc ? (pssucc ? psone)
120  | pssucc _ p' ⇒ pssucc ? (pssucc ? (pssucc ? (possucc0 ? p')))
121  ].
122
[487]123let rec possuccinj (n:Pos) : possucc n ≝
[10]124  match n with
125  [ one ⇒ psone
126  | p0 ps ⇒ possucc0 ? (possuccinj ps)
127  | p1 ps ⇒ possucc1 ? (possuccinj ps)
128  ].
129
[487]130let rec possucc_elim
[10]131  (P : Pos → Prop)
132  (Pone : P one)
133  (Psucc : ∀n. P n → P (succ n))
134  (n : Pos)
135  (p:possucc n) on p : P n ≝
136  match p with
137  [ psone ⇒ Pone
138  | pssucc _ p' ⇒ Psucc ? (possucc_elim P Pone Psucc ? p')
139  ].
140
[487]141definition pos_elim : ∀P:Pos → Prop. P one → (∀n. P n → P (succ n)) → ∀n. P n.
142#P #Pone #Psucc #n @(possucc_elim … (possuccinj n)) /2/; qed.
[10]143
[487]144let rec possucc_cases
[10]145  (P : Pos → Prop)
146  (Pone : P one)
147  (Psucc : ∀n. P (succ n))
148  (n : Pos)
149  (p:possucc n) on p : P n ≝
150  match p with
151  [ psone ⇒ Pone
152  | pssucc _ p' ⇒ Psucc ?
153  ].
154
[487]155definition pos_cases : ∀P:Pos → Prop. P one → (∀n. P (succ n)) → ∀n. P n.
156#P #Pone #Psucc #n @(possucc_cases … (possuccinj n)) /2/; qed.
[10]157
[487]158theorem succ_pred_n : ∀n. n≠one → n = succ (pred n).
159@pos_elim
160[ #H @False_ind elim H; /2/;
161| //;
162] qed.
[10]163
[487]164theorem not_eq_one_succ : ∀n:Pos. one ≠ succ n.
165#n elim n; normalize;
166[ % #H destruct;
167| 2,3: #n' #H % #H' destruct;
168] qed.
[10]169
[487]170theorem not_eq_n_succn: ∀n:Pos. n ≠ succ n.
171#n elim n;
172[ //;
173| *: #n' #IH normalize; % #H destruct
174] qed.
[10]175
[487]176theorem pos_elim2:
[10]177 ∀R:Pos → Pos → Prop.
178  (∀n:Pos. R one n)
179  → (∀n:Pos. R (succ n) one)
180  → (∀n,m:Pos. R n m → R (succ n) (succ m))
181  → ∀n,m:Pos. R n m.
[487]182#R #ROn #RSO #RSS @pos_elim //;
183#n0 #Rn0m @pos_elim /2/; qed.
[10]184
185
[487]186theorem decidable_eq_pos: ∀n,m:Pos. decidable (n=m).
187@pos_elim2 #n
188[ @(pos_elim ??? n) /2/;
189| /3/;
190| #m #Hind cases Hind; /3/;
191] qed.
[10]192
[487]193let rec plus n m ≝
[10]194  match n with
195  [ one ⇒ succ m
196  | p0 n' ⇒
197    match m with
198    [ one ⇒ p1 n'
199    | p0 m' ⇒ p0 (plus n' m')
200    | p1 m' ⇒ p1 (plus n' m')
201    ]
202  | p1 n' ⇒
203    match m with
204    [ one ⇒ succ n
205    | p0 m' ⇒ p1 (plus n' m')
206    | p1 m' ⇒ p0 (succ (plus n' m'))
207    ]
208  ].
209
210interpretation "positive plus" 'plus x y = (plus x y).
211
[487]212theorem plus_n_succm: ∀n,m. succ (n + m) = n + (succ m).
213#n elim n; normalize;
214[ //
[1517]215| 2,3: #n' #IH #m cases m; /3 by eq_f, sym_eq/
216    normalize; cases n' //
[487]217] qed.
[10]218
[1528]219theorem commutative_plus_pos : commutative ? plus.
[487]220#n elim n;
221[ #y cases y; normalize; //;
222| 2,3: #n' #IH #y cases y; normalize; //;
223] qed.
[10]224
[487]225theorem pluss_succn_m: ∀n,m. succ (n + m) = (succ n) + m.
[1528]226#n #m >(commutative_plus_pos (succ n) m)
[487]227<(plus_n_succm …) //; qed.
[10]228
[487]229theorem associative_plus : associative Pos plus.
230@pos_elim
231[ normalize; //;
232| #x' #IHx @pos_elim
233  [ #z <(pluss_succn_m …) <(pluss_succn_m …)
234      <(pluss_succn_m …) //;
235  | #y' #IHy' #z
236      <(pluss_succn_m y' …)
237      <(plus_n_succm …)
238      <(plus_n_succm …)
239      <(pluss_succn_m ? z) >(IHy' …) //;
240  ]
241] qed.
[10]242
[487]243theorem injective_plus_r: ∀n:Pos.injective Pos Pos (λm.n+m).
244@pos_elim normalize; /3/; qed.
[10]245
[487]246theorem injective_plus_l: ∀n:Pos.injective Pos Pos (λm.m+n).
247/2/; qed.
[10]248
[487]249theorem nat_plus_pos_plus: ∀n,m:nat. succ_pos_of_nat (n+m) = pred (succ_pos_of_nat n + succ_pos_of_nat m).
250#n elim n;
251[ normalize; //;
252| #n' #IH #m normalize; >(IH m) <(pluss_succn_m …)
253    <(pred_succ_n ?) <(succ_pred_n …) //;
254    elim n'; normalize; /2/;
255] qed.
[10]256
[487]257let rec times n m ≝
[10]258match n with
259[ one ⇒ m
260| p0 n' ⇒ p0 (times n' m)
261| p1 n' ⇒ m + p0 (times n' m)
262].
263
264interpretation "positive times" 'times x y = (times x y).
265
[487]266lemma p0_times2: ∀n. p0 n = (succ one) * n.
267//; qed.
[10]268
[487]269lemma plus_times2: ∀n. n + n = (succ one) * n.
270#n elim n;
271[ //;
272| 2,3: #n' #IH normalize; >IH //;
273] qed.
[10]274
275
[487]276theorem times_succn_m: ∀n,m. m+n*m = (succ n)*m.
277#n elim n;
278[ /2/
279| #n' #IH normalize; #m <(IH m) //;
280| /2/
281] qed.
[10]282
[487]283theorem times_n_succm: ∀n,m:Pos. n+(n*m) = n*(succ m).
284@pos_elim
285[ //
[1517]286| #n #IH #m <(times_succn_m …) <(times_succn_m …) /3 by succ_injective, trans_eq/
[487]287] qed.
[10]288
[487]289theorem times_n_one: ∀n:Pos. n * one = n.
290#n elim n; /3/; qed.
[10]291
[487]292theorem commutative_times: commutative Pos times.
293@pos_elim /2/; qed.
[10]294
[487]295theorem distributive_times_plus : distributive Pos times plus.
296@pos_elim /2/; qed.
[10]297
[487]298theorem distributive_times_plus_r: ∀a,b,c:Pos. (b+c)*a = b*a + c*a.
299//; qed.
[10]300
[487]301theorem associative_times: associative Pos times.
302@pos_elim
303[ //;
304| #x #IH #y #z <(times_succn_m …) <(times_succn_m …) //;
305] qed.
[10]306
[487]307lemma times_times: ∀x,y,z:Pos. x*(y*z) = y*(x*z).
308//; qed.
[10]309
310(*** ordering relations ***)
311
312(* sticking closely to the unary version; not sure if this is a good idea,
313   but it means the proofs are much the same. *)
314
[487]315inductive le (n:Pos) : Pos → Prop ≝
[10]316  | le_n : le n n
317  | le_S : ∀m:Pos. le n m → le n (succ m).
318
319interpretation "positive 'less than or equal to'" 'leq x y = (le x y).
320interpretation "positive 'neither less than or equal to'" 'nleq x y = (Not (le x y)).
321
[487]322definition lt: Pos → Pos → Prop ≝ λn,m. succ n ≤ m.
[10]323
324interpretation "positive 'less than'" 'lt x y = (lt x y).
325interpretation "positive 'not less than'" 'nless x y = (Not (lt x y)).
326
[487]327definition ge: Pos → Pos → Prop ≝ λn,m:Pos. m ≤ n.
[10]328
329interpretation "positive 'greater than or equal to'" 'geq x y = (ge x y).
330interpretation "positive 'neither greater than or equal to'" 'ngeq x y = (Not (ge x y)).
331
[487]332definition gt: Pos → Pos → Prop ≝ λn,m. m<n.
[10]333
334interpretation "positive 'greater than'" 'gt x y = (gt x y).
335interpretation "positive 'not greater than'" 'ngtr x y = (Not (gt x y)).
336
[487]337theorem transitive_le: transitive Pos le.
338#a #b #c #leab #lebc elim lebc; /2/; qed.
[10]339
[487]340theorem transitive_lt: transitive Pos lt.
341#a #b #c #ltab #ltbc elim ltbc; /2/; qed.
[10]342
[487]343theorem le_succ_succ: ∀n,m:Pos. n ≤ m → succ n ≤ succ m.
344#n #m #lenm elim lenm; /2/; qed.
[10]345
[487]346theorem le_one_n : ∀n:Pos. one ≤ n.
347@pos_elim /2/; qed.
[10]348
[487]349theorem le_n_succn : ∀n:Pos. n ≤ succ n.
350/2/; qed.
[10]351
[487]352theorem le_pred_n : ∀n:Pos. pred n ≤ n.
353@pos_elim //; qed.
[10]354
[487]355theorem monotonic_pred: monotonic Pos le pred.
356#n #m #lenm elim lenm; /2/;qed.
[10]357
[487]358theorem le_S_S_to_le: ∀n,m:Pos. succ n ≤ succ m → n ≤ m.
359/2/; qed.
[10]360
361(* lt vs. le *)
[487]362theorem not_le_succ_one: ∀ n:Pos. succ n ≰ one.
363#n % #H inversion H /2/; qed.
[10]364
[487]365theorem not_le_to_not_le_succ_succ: ∀ n,m:Pos. n ≰ m → succ n ≰ succ m.
[697]366#n #m @not_to_not @le_S_S_to_le qed.
[10]367
[487]368theorem not_le_succ_succ_to_not_le: ∀ n,m:Pos. succ n ≰ succ m → n ≰ m.
[697]369#n #m @not_to_not /2/ qed.
[10]370
[487]371theorem decidable_le: ∀n,m:Pos. decidable (n≤m).
372@pos_elim2 #n /2/;
373#m *; /3/; qed.
[10]374
[487]375theorem decidable_lt: ∀n,m:Pos. decidable (n < m).
376#n #m @decidable_le  qed.
[10]377
[487]378theorem not_le_succ_n: ∀n:Pos. succ n ≰ n.
379@pos_elim //;
380#m #IH @not_le_to_not_le_succ_succ //;
381qed.
[10]382
[487]383theorem not_le_to_lt: ∀n,m:Pos. n ≰ m → m < n.
384@pos_elim2 #n
385 [#abs @False_ind /2/;
386 |/2/;
387 |#m #Hind #HnotleSS @le_succ_succ /3/;
388 ]
389qed.
[10]390
[487]391theorem lt_to_not_le: ∀n,m:Pos. n < m → m ≰ n.
392#n #m #Hltnm elim Hltnm;
393[ //
394| #p #H @not_to_not /2/;
395] qed.
[10]396
[487]397theorem not_lt_to_le: ∀n,m:Pos. n ≮ m → m ≤ n.
398/4/; qed.
[10]399
400
[487]401theorem le_to_not_lt: ∀n,m:Pos. n ≤ m → m ≮ n.
402#n #m #H @lt_to_not_le /2/;qed.
[10]403
404(* lt and le trans *)
405
[487]406theorem lt_to_le_to_lt: ∀n,m,p:Pos. n < m → m ≤ p → n < p.
407#n #m #p #H #H1 elim H1; /2/; qed.
[10]408
[487]409theorem le_to_lt_to_lt: ∀n,m,p:Pos. n ≤ m → m < p → n < p.
410#n #m #p #H elim H; /3/; qed.
[10]411
[487]412theorem lt_succ_to_lt: ∀n,m:Pos. succ n < m → n < m.
413/2/; qed.
[10]414
[487]415theorem ltn_to_lt_one: ∀n,m:Pos. n < m → one < m.
416/2/; qed.
[10]417
[487]418theorem lt_one_n_elim: ∀n:Pos. one < n →
[10]419  ∀P:Pos → Prop.(∀m:Pos.P (succ m)) → P n.
[487]420@pos_elim //; #abs @False_ind /2/;
421qed.
[10]422
423(* le to lt or eq *)
[487]424theorem le_to_or_lt_eq: ∀n,m:Pos. n ≤ m → n < m ∨ n = m.
425#n #m #lenm elim lenm; /3/; qed.
[10]426
427(* not eq *)
[487]428theorem lt_to_not_eq : ∀n,m:Pos. n < m → n ≠ m.
429#n #m #H @not_to_not /2/; qed.
[10]430
[487]431theorem not_eq_to_le_to_lt: ∀n,m:Pos. n≠m → n≤m → n<m.
432#n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle); //;
433#Heq /3/; qed.
[10]434
435(* le elimination *)
[487]436theorem le_n_one_to_eq : ∀n:Pos. n ≤ one → one=n.
437@pos_cases //; #a ; #abs
438@False_ind /2/;qed.
[10]439
[487]440theorem le_n_one_elim: ∀n:Pos. n ≤ one → ∀P: Pos →Prop. P one → P n.
441@pos_cases //; #a #abs
442@False_ind /2/; qed.
[10]443
[487]444theorem le_n_Sm_elim : ∀n,m:Pos.n ≤ succ m →
[10]445∀P:Prop. (succ n ≤ succ m → P) → (n=succ m → P) → P.
[487]446#n #m #Hle #P elim Hle; /3/; qed.
[10]447
448(* le and eq *)
449
[487]450theorem le_to_le_to_eq: ∀n,m:Pos. n ≤ m → m ≤ n → n = m.
[1517]451@pos_elim2 /4 by le_n_one_to_eq, monotonic_pred, eq_f, sym_eq/
[487]452qed.
[10]453
[487]454theorem lt_one_S : ∀n:Pos. one < succ n.
455/2/; qed.
[10]456
457(* well founded induction principles *)
458
[487]459theorem pos_elim1 : ∀n:Pos.∀P:Pos → Prop.
[10]460(∀m.(∀p. p < m → P p) → P m) → P n.
[487]461#n #P #H
462cut (∀q:Pos. q ≤ n → P q);/2/;
463@(pos_elim … n)
464 [#q #HleO (* applica male *)
465    @(le_n_one_elim ? HleO)
466    @H #p #ltpO
467    @False_ind /2/; (* 3 *)
468 |#p #Hind #q #HleS
469    @H #a #lta @Hind
470    @le_S_S_to_le /2/;
471 ]
472qed.
[10]473
474(*********************** monotonicity ***************************)
[487]475theorem monotonic_le_plus_r:
[10]476∀n:Pos.monotonic Pos le (λm.n + m).
[487]477#n #a #b @(pos_elim … n) normalize; /2/;
478#m #H #leab /3/; qed.
[10]479
[487]480theorem monotonic_le_plus_l:
[10]481∀m:Pos.monotonic Pos le (λn.n + m).
[487]482/2/; qed.
[10]483
[487]484theorem le_plus: ∀n1,n2,m1,m2:Pos. n1 ≤ n2  → m1 ≤ m2
[10]485→ n1 + m1 ≤ n2 + m2.
[487]486#n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
487/2/; qed.
[10]488
[487]489theorem le_plus_n :∀n,m:Pos. m ≤ n + m.
490/3/; qed.
[10]491
[487]492lemma le_plus_a: ∀a,n,m:Pos. n ≤ m → n ≤ a + m.
493/2/; qed.
[10]494
[487]495lemma le_plus_b: ∀b,n,m:Pos. n + b ≤ m → n ≤ m.
496/2/; qed.
[10]497
[487]498theorem le_plus_n_r :∀n,m:Pos. m ≤ m + n.
499/2/; qed.
[10]500
[487]501theorem eq_plus_to_le: ∀n,m,p:Pos.n=m+p → m ≤ n.
502//; qed.
[10]503
[487]504theorem le_plus_to_le: ∀a,n,m:Pos. a + n ≤ a + m → n ≤ m.
505@pos_elim normalize; /3/; qed.
[10]506
[487]507theorem le_plus_to_le_r: ∀a,n,m:Pos. n + a ≤ m +a → n ≤ m.
508/2/; qed.
[10]509
510(* plus & lt *)
511
[487]512theorem monotonic_lt_plus_r:
[10]513∀n:Pos.monotonic Pos lt (λm.n+m).
[487]514/2/; qed.
[10]515
[487]516theorem monotonic_lt_plus_l:
[10]517∀n:Pos.monotonic Pos lt (λm.m+n).
[487]518/2/; qed.
[10]519
[487]520theorem lt_plus: ∀n,m,p,q:Pos. n < m → p < q → n + p < m + q.
521#n #m #p #q #ltnm #ltpq
522@(transitive_lt ? (n+q)) /2/; qed.
[10]523
[487]524theorem le_lt_plus_pos: ∀n,m,p:Pos. n ≤ m → n < m + p.
525#n #m #p #H @(le_to_lt_to_lt … H)
526/2/; qed.
[10]527
[487]528theorem lt_plus_to_lt_l :∀n,p,q:Pos. p+n < q+n → p<q.
529/2/; qed.
[10]530
[487]531theorem lt_plus_to_lt_r :∀n,p,q:Pos. n+p < n+q → p<q.
532/2/; qed.
[10]533
534(* times *)
[487]535theorem monotonic_le_times_r:
[10]536∀n:Pos.monotonic Pos le (λm. n * m).
[487]537#n #x #y #lexy @(pos_elim … n) normalize;//;(* lento /2/;*)
538#a #lea /2/;
539qed.
[10]540
[487]541theorem le_times: ∀n1,n2,m1,m2:Pos.
[10]542n1 ≤ n2  → m1 ≤ m2 → n1*m1 ≤ n2*m2.
[487]543#n1 #n2 #m1 #m2 #len #lem
544@(transitive_le ? (n1*m2)) (* /2/ slow *)
545 [ @monotonic_le_times_r //;
546 | applyS monotonic_le_times_r;//;
547 ]
548qed.
[10]549
[487]550theorem lt_times_n: ∀n,m:Pos. m ≤ n*m.
551#n #m /2/; qed.
[10]552
[487]553theorem le_times_to_le:
[10]554∀a,n,m:Pos. a * n ≤ a * m → n ≤ m.
[487]555#a @pos_elim2 normalize;
556  [//;
557  |#n >(times_n_one …) <(times_n_succm …)
558     #H @False_ind
559     elim (lt_to_not_le ?? (le_lt_plus_pos a a (a*n) …)); /2/;
560  |#n #m #H #le
561     @le_succ_succ @H /2/;
562  ]
563qed.
[10]564
[487]565theorem le_S_times_2: ∀n,m:Pos. n ≤ m → succ n ≤ (succ one)*m.
566#n #m #lenm  (* interessante *)
567applyS (le_plus n m); //; qed.
[10]568
569(* prove injectivity of times from above *)
[487]570theorem injective_times_r: ∀n:Pos.injective Pos Pos (λm.n*m).
571#n #m #p #H @le_to_le_to_eq
[10]572/2/;
[487]573qed.
[10]574
[487]575theorem injective_times_l: ∀n:Pos.injective Pos Pos (λm.m*n).
576/2/; qed.
[10]577
578(* times & lt *)
579
[487]580theorem monotonic_lt_times_l:
[10]581  ∀c:Pos. monotonic Pos lt (λt.(t*c)).
[487]582#c #n #m #ltnm
583elim ltnm; normalize;
584  [/2/;
585  |#a #_ #lt1 @(transitive_le ??? lt1) //;
586  ]
587qed.
[10]588
[487]589theorem monotonic_lt_times_r:
[10]590  ∀c:Pos. monotonic Pos lt (λt.(c*t)).
[487]591#a #b #c #H
592>(commutative_times a b) >(commutative_times a c)
593/2/; qed.
[10]594
[487]595theorem lt_to_le_to_lt_times:
[10]596∀n,m,p,q:Pos. n < m → p ≤ q → n*p < m*q.
[487]597#n #m #p #q #ltnm #lepq
598@(le_to_lt_to_lt ? (n*q))
599  [@monotonic_le_times_r //;
600  |@monotonic_lt_times_l //;
601  ]
602qed.
[10]603
[487]604theorem lt_times:∀n,m,p,q:Pos. n<m → p<q → n*p < m*q.
605#n #m #p #q #ltnm #ltpq
606@lt_to_le_to_lt_times /2/;
607qed.
[10]608
[487]609theorem lt_times_n_to_lt_l:
[10]610∀n,p,q:Pos. p*n < q*n → p < q.
[487]611#n #p #q #Hlt
612elim (decidable_lt p q);//;
613#nltpq @False_ind
614@(absurd ? ? (lt_to_not_le ? ? Hlt))
615applyS monotonic_le_times_r;/2/;
616qed.
[10]617
[487]618theorem lt_times_n_to_lt_r:
[10]619∀n,p,q:Pos. n*p < n*q → p < q.
[487]620/2/; qed.
[10]621
622(**** minus ****)
623
[487]624inductive minusresult : Type[0] ≝
[10]625 | MinusNeg: minusresult
626 | MinusZero: minusresult
627 | MinusPos: Pos → minusresult.
628
[487]629let rec partial_minus (n,m:Pos) : minusresult ≝
[10]630match n with
631[ one ⇒ match m with [ one ⇒ MinusZero | _ ⇒ MinusNeg ]
632| p0 n' ⇒
633  match m with
634  [ one ⇒ MinusPos (pred n)
635  | p0 m' ⇒ match partial_minus n' m' with
636            [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusZero | MinusPos p ⇒ MinusPos (p0 p) ]
637  | p1 m' ⇒ match partial_minus n' m' with
638            [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusNeg | MinusPos p ⇒ MinusPos (pred (p0 p)) ]
639  ]
640| p1 n' ⇒
641  match m with
642  [ one ⇒ MinusPos (p0 n')
643  | p0 m' ⇒ match partial_minus n' m' with
644            [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusPos one | MinusPos p ⇒ MinusPos (p1 p) ]
645  | p1 m' ⇒ match partial_minus n' m' with
646            [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusZero | MinusPos p ⇒ MinusPos (p0 p) ]
647  ]
648].
649
[487]650example testminus0: partial_minus (p0 one) (p1 one) = MinusNeg. //; qed.
651example testminus1: partial_minus (p0 one) (p0 (p0 one)) = MinusNeg. //; qed.
652example testminus2: partial_minus (p0 (p0 one)) (p0 one) = MinusPos (p0 one). //; qed.
653example testminus3: partial_minus (p0 one) one = MinusPos one. //; qed.
654example testminus4: partial_minus (succ (p1 one)) (p1 one) = MinusPos one. //; qed.
[10]655
[487]656definition minus ≝ λn,m. match partial_minus n m with [ MinusPos p ⇒ p | _ ⇒ one ].
[10]657
[1515]658interpretation "positive minus" 'minus x y = (minus x y).
[10]659
[487]660lemma partialminus_S: ∀n,m:Pos.
[10]661match partial_minus (succ n) m with
662[ MinusPos p ⇒ match p with [ one ⇒ partial_minus n m = MinusZero | _ ⇒ partial_minus n m = MinusPos (pred p) ]
663| _ ⇒ partial_minus n m = MinusNeg
664].
[487]665#n elim n;
666[ #m cases m;
667  [ //;
668  | 2,3: #m' cases m'; //;
669  ]
[10]670(* The other two cases are the same.  I'd combine them, but the numbering
671   would be even more horrific. *)
[487]672| #n' #IH #m cases m;
673  [ normalize; <(pred_succ_n n') cases n'; //;
674  | 2,3: #m' normalize; lapply (IH m'); cases (partial_minus (succ n') m');
675    [ 1,2,4,5: normalize; #H >H //;
676    | 3,6: #p cases p; [ 1,4: normalize; #H >H //;
677                      | 2,3,5,6: #p' normalize; #H >H //;
678                      ]
679    ]
680  ]
681| #n' #IH #m cases m;
682  [ normalize; <(pred_succ_n n') cases n'; //;
683  | 2,3: #m' normalize; lapply (IH m'); cases (partial_minus (succ n') m');
684    [ 1,2,4,5: normalize; #H >H //;
685    | 3,6: #p cases p; [ 1,4: normalize; #H >H //;
686                      | 2,3,5,6: #p' normalize; #H >H //;
687                      ]
688    ]
689  ]
690] qed.
[10]691
[487]692lemma partialminus_n_S: ∀n,m:Pos.
[10]693  match partial_minus n m with
694  [ MinusPos p ⇒ match p with [ one ⇒ partial_minus n (succ m) = MinusZero
695                              | _ ⇒ partial_minus n (succ m) = MinusPos (pred p)
696                              ]
697  | _ ⇒ partial_minus n (succ m) = MinusNeg
698  ].
[487]699#n elim n;
700[ #m cases m; //;
[10]701(* Again, lots of unnecessary duplication! *)
[487]702| #n' #IH #m cases m;
703  [ normalize; cases n'; //;
704  | #m' normalize; lapply (IH m'); cases (partial_minus n' m');
705    [ 1,2: normalize; #H >H //;
706    | #p cases p; normalize; [ #H >H //;
707                                  | 2,3: #p' #H >H //;
708                                  ]
709    ]
710  |  #m' normalize; lapply (IH m'); cases (partial_minus n' m');
711    [ 1,2: normalize; #H >H //;
712    | #p cases p; normalize; [ #H >H //;
713                                  | 2,3: #p' #H >H //;
714                                  ]
715    ]
716  ]
717| #n' #IH #m cases m;
718  [ normalize; cases n'; //;
719  | #m' normalize; lapply (IH m'); cases (partial_minus n' m');
720    [ 1,2: normalize; #H >H //;
721    | #p cases p; normalize; [ #H >H //;
722                                  | 2,3: #p' #H >H //;
723                                  ]
724    ]
725  |  #m' normalize; lapply (IH m'); cases (partial_minus n' m');
726    [ 1,2: normalize; #H >H //;
727    | #p cases p; normalize; [ #H >H //;
728                                  | 2,3: #p' #H >H //;
729                                  ]
730    ]
731  ]
732] qed.
[10]733
[487]734theorem partialminus_S_S: ∀n,m:Pos. partial_minus (succ n) (succ m) = partial_minus n m.
735#n elim n;
736[ #m cases m;
737  [ //;
738  | 2,3: #m' cases m'; //;
739  ]
740| #n' #IH #m cases m;
741  [ normalize; cases n'; /2/; normalize; #n'' <(pred_succ_n n'') cases n'';//;
742  | #m' normalize; >(IH ?) //;
743  | #m' normalize; lapply (partialminus_S n' m'); cases (partial_minus (succ n') m');
744    [ 1,2: normalize; #H >H //;
745    | #p cases p; [ normalize; #H >H //;
746                      | 2,3: #p' normalize; #H >H //;
747                      ]
748    ]
749  ]
750|  #n' #IH #m cases m;
751  [ normalize; cases n'; /2/;
752  | #m' normalize; lapply (partialminus_n_S n' m'); cases (partial_minus n' m');
753    [ 1,2: normalize; #H >H //;
754    | #p cases p;   [ normalize; #H >H //;
755                      | 2,3: #p' normalize; #H >H //;
756                      ]
757    ]
758  | #m' normalize; >(IH ?) //;
759  ]
760] qed.
[10]761
[487]762theorem minus_S_S: ∀n,m:Pos. (succ n) - (succ m) = n-m.
763#n #m normalize; >(partialminus_S_S n m) //; qed.
[10]764
[487]765theorem minus_one_n: ∀n:Pos.one=one-n.
766#n cases n; //; qed.
[10]767
[487]768theorem minus_n_one: ∀n:Pos.pred n=n-one.
769#n cases n; //; qed.
[10]770
[487]771lemma partial_minus_n_n: ∀n. partial_minus n n = MinusZero.
772#n elim n;
773[ //;
774| 2,3: normalize; #n' #IH >IH //
775] qed.
[10]776
[1528]777theorem minus_n_n_pos: ∀n:Pos.one=n-n.
[487]778#n normalize; >(partial_minus_n_n n) //;
779qed.
[10]780
[487]781theorem minus_Sn_n: ∀n:Pos. one = (succ n)-n.
782#n cut (partial_minus (succ n) n = MinusPos one);
783[ elim n;
784  [ //;
785  | normalize; #n' #IH >IH //;
786  | normalize; #n' #IH >(partial_minus_n_n n') //;
787  ]
788| #H normalize; >H //;
789] qed.
[10]790
[487]791theorem minus_Sn_m: ∀m,n:Pos. m < n → succ n -m = succ (n-m).
[10]792(* qualcosa da capire qui
[487]793#n #m #lenm elim lenm; napplyS refl_eq. *)
794@pos_elim2
795  [#n #H @(lt_one_n_elim n H) //;
796  |#n #abs @False_ind /2/
797  |#n #m #Hind #c applyS Hind; /2/;
798  ]
799qed.
[10]800
[487]801theorem not_eq_to_le_to_le_minus:
[10]802  ∀n,m:Pos.n ≠ m → n ≤ m → n ≤ m - one.
[487]803#n @pos_cases //; #m
804#H #H1 @le_S_S_to_le
805applyS (not_eq_to_le_to_lt n (succ m) H H1);
806qed.
[10]807
[487]808theorem eq_minus_S_pred: ∀n,m:Pos. n - (succ m) = pred(n -m).
809@pos_elim2
810[ #n cases n; normalize; //;
811| #n @(pos_elim … n) //;
812| //;
813] qed.
[10]814
[487]815lemma pred_Sn_plus: ∀n,m:Pos. one < n → (pred n)+m = pred (n+m).
816#n #m #H
817@(lt_one_n_elim … H) /3/;
818qed.
[10]819
[487]820theorem plus_minus:
[10]821∀m,n,p:Pos. m < n → (n-m)+p = (n+p)-m.
[487]822@pos_elim2
823  [ #n #p #H <(minus_n_one ?) <(minus_n_one ?) /2/;
824  |#n #p #abs @False_ind /2/;
825  |#n #m #IH #p #H >(eq_minus_S_pred …) >(eq_minus_S_pred …)
826     cut (n<m); [ /2/ ] #H'
827     >(pred_Sn_plus …)
828     [ >(minus_Sn_m …) /2/;
829         <(pluss_succn_m …)
830         <(pluss_succn_m …)
831         >(minus_Sn_m …)
832         [ <(pred_succ_n …)
833             <(pred_succ_n …)
834             @IH /2/;
835         | /2/;
836         ]
837     | >(minus_Sn_m … H') //;
838     ]
839  ] qed.
[10]840
841(* XXX: putting this in the appropriate case screws up auto?! *)
[487]842theorem succ_plus_one: ∀n. succ n = n + one.
843#n elim n; //; qed.
[10]844
[487]845theorem nat_possucc: ∀p. nat_of_pos (succ p) = S (nat_of_pos p).
846#p elim p; normalize;
847[ //;
848| #q #IH <(plus_n_O …) <(plus_n_O …)
849    >IH <(plus_n_Sm …) //;
850| //;
851] qed.
[10]852
[487]853theorem nat_succ_pos: ∀n. nat_of_pos (succ_pos_of_nat n) = S n.
854#n elim n; //; qed.
[10]855
[487]856theorem minus_plus_m_m: ∀n,m:Pos.n = (n+m)-m.
857#n @pos_elim
858[ //;
859| #m #IH <(plus_n_succm …)
860    >(eq_minus_S_pred …)
861    >(minus_Sn_m …) /2/;
862] qed.
[10]863
[487]864theorem plus_minus_m_m: ∀n,m:Pos.
[10]865  m < n → n = (n-m)+m.
[487]866#n #m #lemn applyS sym_eq;
867applyS (plus_minus m n m); //; qed.
[10]868
[487]869theorem le_plus_minus_m_m: ∀n,m:Pos. n ≤ (n-m)+m.
870@pos_elim
871  [//
872  |#a #Hind @pos_cases //; 
873     #n
874     >(minus_S_S …)
[10]875     /2/;
[487]876  ]
877qed.
[10]878
[1528]879theorem minus_to_plus_pos :∀n,m,p:Pos.
[10]880  m < n → n-m = p → n = m+p.
[487]881#n #m #p #lemn #eqp applyS plus_minus_m_m; //;
882qed.
[10]883
[1528]884theorem plus_to_minus_pos :∀n,m,p:Pos.n = m+p → n-m = p.
[10]885(* /4/ done in 43.5 *)
[487]886#n #m #p #eqp
887@sym_eq
888applyS (minus_plus_m_m p m);
889qed.
[10]890
[487]891theorem minus_pred_pred : ∀n,m:Pos. one < n → one < m →
[10]892pred n - pred m = n - m.
[487]893#n #m #posn #posm
894@(lt_one_n_elim n posn)
895@(lt_one_n_elim m posm) //.
896qed.
[10]897
898(* monotonicity and galois *)
899
[487]900theorem monotonic_le_minus_l:
[10]901∀p,q,n:Pos. q ≤ p → q-n ≤ p-n.
[487]902@pos_elim2 #p #q
903  [#lePO @(le_n_one_elim ? lePO) //;
904  |//;
905  |#Hind @pos_cases
906    [/2/;
907    |#a #leSS >(minus_S_S …) >(minus_S_S …) @Hind /2/;
908    ]
909  ]
910qed.
[10]911
[487]912theorem le_minus_to_plus: ∀n,m,p:Pos. n-m ≤ p → n≤ p+m.
913#n #m #p #lep
914@transitive_le
[1517]915  [|@le_plus_minus_m_m
[487]916  |@monotonic_le_plus_l //;
917  ]
918qed.
[10]919
[487]920theorem le_plus_to_minus: ∀n,m,p:Pos. n ≤ p+m → n-m ≤ p.
921#n #m #p #lep
[10]922(* bello *)
[487]923applyS monotonic_le_minus_l;//;
[10]924(* /2/; *)
[487]925qed.
[10]926
[487]927theorem monotonic_le_minus_r:
[10]928∀p,q,n:Pos. q ≤ p → n-p ≤ n-q.
[487]929#p #q #n #lepq
930@le_plus_to_minus
931@(transitive_le ??? (le_plus_minus_m_m ? q)) /2/;
932qed.
[10]933
934(*********************** boolean arithmetics ********************)
935include "basics/bool.ma".
936
[487]937let rec eqb n m ≝
[10]938match n with
939  [ one ⇒ match m with [ one ⇒ true | _ ⇒ false]
940  | p0 p ⇒ match m with [ p0 q ⇒ eqb p q | _ ⇒ false]
941  | p1 p ⇒ match m with [ p1 q ⇒ eqb p q | _ ⇒ false]
942  ].
[487]943
[1515]944theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Type[0].
[10]945(n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)).
[487]946#n elim n;
947[ #m cases m normalize
948  [ /2/
949  | 2,3: #m' #P #t #f @f % #H destruct
950  ]
951| #n' #IH #m cases m normalize
952  [ #P #t #f @f % #H destruct
953  | #m' #P #t #f @IH
954    [ /2/
955    | * #ne @f % #e @ne destruct @refl
956    ]
957  | #m' #P #t #f @f % #H destruct;
958  ]
959| #n' #IH #m cases m; normalize;
960  [ #P #t #f @f % #H destruct;
961  | #m' #P #t #f @f % #H destruct;
962  | #m' #P #t #f @IH
963    [ /2/;
964    | * #ne @f % #e @ne destruct @refl
965    ]
966  ]
967] qed.
[10]968
[487]969theorem eqb_n_n: ∀n:Pos. eqb n n = true.
970#n elim n; normalize; //.
971qed.
[10]972
[487]973theorem eqb_true_to_eq: ∀n,m:Pos. eqb n m = true → n = m.
974#n #m @(eqb_elim n m) //;
975#_ #abs @False_ind /2/;
976qed.
[10]977
[487]978theorem eqb_false_to_not_eq: ∀n,m:Pos. eqb n m = false → n ≠ m.
979#n #m @(eqb_elim n m) /2/;
980qed.
[10]981
[487]982theorem eq_to_eqb_true: ∀n,m:Pos.
[10]983  n = m → eqb n m = true.
[487]984//; qed.
[10]985
[487]986theorem not_eq_to_eqb_false: ∀n,m:Pos.
[10]987  n ≠  m → eqb n m = false.
[487]988#n #m #noteq
989@eqb_elim //;
990#Heq @False_ind /2/;
991qed.
[10]992
[487]993let rec leb n m ≝
[10]994match partial_minus n m with
995[ MinusNeg ⇒ true
996| MinusZero ⇒ true
997| MinusPos _ ⇒ false
998].
999
[487]1000lemma leb_unfold_hack: ∀n,m:Pos. leb n m =
[10]1001match partial_minus n m with
1002[ MinusNeg ⇒ true
1003| MinusZero ⇒ true
1004| MinusPos _ ⇒ false
[487]1005]. #n #m (* XXX: why on earth do I need to case split? *) cases n; //; qed.
[10]1006
[487]1007theorem leb_elim: ∀n,m:Pos. ∀P:bool → Prop.
[10]1008(n ≤ m → P true) → (n ≰ m → P false) → P (leb n m).
[487]1009@pos_elim2
1010[ #n cases n; normalize; /2/;
1011| #n cases n; normalize;
1012  [ /2/;
1013  | 2,3: #m' #P #t #f @f /2/; % #H inversion H;
1014    [ #H' destruct;
1015    | #p /2/;
1016    ]
1017  ]
1018| #n #m #IH #P #t #f >(leb_unfold_hack …)
1019    >(partialminus_S_S n m)
1020    <(leb_unfold_hack …)
1021    @IH #H /3/;
1022] qed.
[10]1023
[487]1024theorem leb_true_to_le:∀n,m:Pos.leb n m = true → n ≤ m.
1025#n #m @leb_elim
1026  [//;
1027  |#_ #abs @False_ind /2/;
1028  ]
1029qed.
[10]1030
[487]1031theorem leb_false_to_not_le:∀n,m:Pos.
[10]1032  leb n m = false → n ≰ m.
[487]1033#n #m @leb_elim
1034  [#_ #abs @False_ind /2/;
1035  |//;
1036  ]
1037qed.
[10]1038
[487]1039theorem le_to_leb_true: ∀n,m:Pos. n ≤ m → leb n m = true.
1040#n #m @leb_elim //;
1041#H #H1 @False_ind /2/;
1042qed.
[10]1043
[487]1044theorem not_le_to_leb_false: ∀n,m:Pos. n ≰ m → leb n m = false.
1045#n #m @leb_elim //;
1046#H #H1 @False_ind /2/;
1047qed.
[10]1048
[487]1049theorem lt_to_leb_false: ∀n,m:Pos. m < n → leb n m = false.
1050/3/; qed.
[10]1051
1052
1053(***** comparison *****)
1054
[487]1055definition pos_compare : Pos → Pos → compare ≝
[10]1056λn,m.match partial_minus n m with
1057[ MinusNeg ⇒ LT
1058| MinusZero ⇒ EQ
1059| MinusPos _ ⇒ GT
1060].
1061
[487]1062theorem pos_compare_n_n: ∀n:Pos. pos_compare n n = EQ.
1063#n normalize; >(partial_minus_n_n n)
1064//; qed.
[10]1065
[487]1066theorem pos_compare_S_S: ∀n,m:Pos.pos_compare n m = pos_compare (succ n) (succ m).
1067#n #m normalize;
1068>(partialminus_S_S …)
[10]1069//;
[487]1070qed.
[10]1071
[487]1072theorem pos_compare_pred_pred:
[10]1073  ∀n,m.one < n → one < m → pos_compare n m = pos_compare (pred n) (pred m).
[487]1074#n #m #Hn #Hm
1075@(lt_one_n_elim n Hn)
1076@(lt_one_n_elim m Hm)
1077#p #q <(pred_succ_n ?) <(pred_succ_n ?)
1078<(pos_compare_S_S …) //;
1079qed.
[10]1080
[487]1081theorem pos_compare_S_one: ∀n:Pos. pos_compare (succ n) one = GT.
1082#n elim n; //; qed.
[10]1083
[487]1084theorem pos_compare_one_S: ∀n:Pos. pos_compare one (succ n) = LT.
1085#n elim n; //; qed.
[10]1086
[487]1087theorem pos_compare_to_Prop:
[10]1088  ∀n,m.match (pos_compare n m) with
1089    [ LT ⇒ n < m
1090    | EQ ⇒ n = m
1091    | GT ⇒ m < n ].
[487]1092#n #m
1093@(pos_elim2 (λn,m.match (pos_compare n m) with
[10]1094  [ LT ⇒ n < m
1095  | EQ ⇒ n = m
[891]1096  | GT ⇒ m < n ]))
[487]1097[1,2:@pos_cases
1098  [ 1,3: /2/;
1099  | 2,4: #m' cases m'; //;
1100  ]
[891]1101|#n1 #m1 <pos_compare_S_S cases (pos_compare n1 m1)
1102   [1,3: #IH @le_succ_succ //
1103   | #IH >IH //
1104   ]
1105]
[487]1106qed.
[10]1107
[487]1108theorem pos_compare_n_m_m_n:
[10]1109  ∀n,m:Pos.pos_compare n m = compare_invert (pos_compare m n).
[487]1110#n #m
1111@(pos_elim2 (λn,m. pos_compare n m = compare_invert (pos_compare m n)))
1112[1,2:#n1 cases n1;/2/;
1113|#n1 #m1
1114<(pos_compare_S_S …)
1115<(pos_compare_S_S …)
1116#IH normalize @IH]
1117qed.
[10]1118     
[487]1119theorem pos_compare_elim :
[10]1120  ∀n,m:Pos. ∀P:compare → Prop.
1121    (n < m → P LT) → (n=m → P EQ) → (m < n → P GT) → P (pos_compare n m).
[487]1122#n #m #P #Hlt #Heq #Hgt
1123cut (match (pos_compare n m) with
[10]1124    [ LT ⇒ n < m
1125    | EQ ⇒ n=m
1126    | GT ⇒ m < n] →
1127  P (pos_compare n m))
[487]1128[cases (pos_compare n m);
1129   [@Hlt
1130   |@Heq
1131   |@Hgt]
1132|#Hcut @Hcut //;
1133qed.
[10]1134
[487]1135inductive cmp_cases (n,m:Pos) : CProp[0] ≝
[10]1136  | cmp_le : n ≤ m → cmp_cases n m
1137  | cmp_gt : m < n → cmp_cases n m.
1138
[487]1139theorem lt_to_le : ∀n,m:Pos. n < m → n ≤ m.
1140/2/; qed.
[10]1141
[487]1142lemma cmp_nat: ∀n,m:Pos.cmp_cases n m.
1143#n #m lapply (pos_compare_to_Prop n m)
[1517]1144cases (pos_compare n m);normalize; /3 by lt_times_n_to_lt_l, le_n, cmp_le, cmp_gt, lt_to_le/
[487]1145qed.
[10]1146
1147
1148
1149
[487]1150let rec two_power_nat (n:nat) : Pos ≝
[10]1151match n with
1152[ O ⇒ one
1153| S n' ⇒ p0 (two_power_nat n')
1154].
1155
[487]1156definition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p).
[1515]1157
1158
1159
1160definition max : Pos → Pos → Pos ≝
1161λn,m. match leb n m with [ true ⇒ m | _ ⇒ n].
[1523]1162
1163
1164
1165lemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
1166#n #m #lt lapply (pos_compare_to_Prop n m); cases (pos_compare n m);
1167[ //;
1168| 2,3: #H @False_ind @(absurd ? lt ?) /3/;
1169] qed.
1170
1171lemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
1172#n #m @eqb_elim //; qed.
Note: See TracBrowser for help on using the repository browser.