summaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
blob: 8525b0e13e8598812cfbb13b7683a0986a0fa4f6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
1507
1508
1509
1510
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)
(*         Benjamin Gregoire, Laurent Thery, INRIA, 2007                *)
(************************************************************************)

Set Implicit Arguments.

Require Import ZArith.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import DoubleBase.
Require Import DoubleDivn1.
Require Import DoubleAdd.
Require Import DoubleSub.

Local Open Scope Z_scope.

Ltac zarith := auto with zarith.


Section POS_MOD.

 Variable w:Type.
 Variable w_0 : w.
 Variable w_digits : positive.
 Variable w_zdigits : w.
 Variable w_WW : w -> w -> zn2z w.
 Variable w_pos_mod : w -> w -> w.
 Variable w_compare : w -> w -> comparison.
 Variable ww_compare : zn2z w -> zn2z w -> comparison.
 Variable w_0W : w ->  zn2z w.
 Variable low: zn2z w -> w.
 Variable ww_sub: zn2z w -> zn2z w -> zn2z w.
 Variable ww_zdigits : zn2z w.


 Definition ww_pos_mod p x :=
  let zdigits := w_0W w_zdigits in
  match x with
  | W0 => W0
  | WW xh xl =>
    match ww_compare p zdigits with
    | Eq => w_WW w_0 xl
    | Lt => w_WW w_0 (w_pos_mod (low p) xl)
    | Gt =>
      match ww_compare p ww_zdigits with
      | Lt =>
        let n := low (ww_sub p zdigits) in
        w_WW (w_pos_mod n xh) xl
      | _ => x
      end
    end
  end.


  Variable w_to_Z : w -> Z.

  Notation wB  := (base w_digits).
  Notation wwB := (base (ww_digits w_digits)).
  Notation "[| x |]" := (w_to_Z x)  (at level 0, x at level 99).

  Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99).


  Variable spec_w_0   : [|w_0|] = 0.

  Variable spec_to_Z  : forall x, 0 <= [|x|] < wB.

  Variable spec_to_w_Z  : forall x, 0 <= [[x]] < wwB.

  Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|].

  Variable spec_pos_mod : forall w p,
       [|w_pos_mod p w|] = [|w|] mod (2 ^ [|p|]).

  Variable spec_w_0W : forall l, [[w_0W l]] = [|l|].
  Variable spec_ww_compare : forall x y,
    ww_compare x y = Z.compare [[x]] [[y]].
 Variable spec_ww_sub: forall x y,
   [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB.

 Variable spec_zdigits : [| w_zdigits |] = Zpos w_digits.
 Variable spec_low: forall x, [| low x|] = [[x]] mod wB.
 Variable spec_ww_zdigits : [[ww_zdigits]] = 2 * [|w_zdigits|].
 Variable spec_ww_digits : ww_digits w_digits = xO w_digits.


  Hint Rewrite spec_w_0 spec_w_WW : w_rewrite.

 Lemma spec_ww_pos_mod : forall w p,
       [[ww_pos_mod p w]] = [[w]] mod (2 ^ [[p]]).
 assert (HHHHH:= lt_0_wB w_digits).
 assert (F0: forall x y, x - y + y = x); auto with zarith.
 intros w1 p; case (spec_to_w_Z p); intros HH1 HH2.
 unfold ww_pos_mod; case w1.
 simpl; rewrite Zmod_small; split; auto with zarith.
 intros xh xl; rewrite spec_ww_compare.
    case Z.compare_spec;
    rewrite spec_w_0W; rewrite spec_zdigits; fold wB;
    intros H1.
   rewrite H1; simpl ww_to_Z.
   autorewrite with w_rewrite rm10.
   rewrite Zplus_mod; auto with zarith.
   rewrite Z_mod_mult; auto with zarith.
   autorewrite with rm10.
   rewrite Zmod_mod; auto with zarith.
   rewrite Zmod_small; auto with zarith.
   autorewrite with w_rewrite rm10.
   simpl ww_to_Z.
   rewrite spec_pos_mod.
   assert (HH0: [|low p|] = [[p]]).
     rewrite spec_low.
     apply Zmod_small; auto with zarith.
     case (spec_to_w_Z p); intros HHH1 HHH2; split; auto with zarith.
     apply Z.lt_le_trans with (1 := H1).
     unfold base; apply Zpower2_le_lin; auto with zarith.
   rewrite HH0.
   rewrite Zplus_mod; auto with zarith.
   unfold base.
   rewrite <- (F0 (Zpos w_digits) [[p]]).
   rewrite Zpower_exp; auto with zarith.
   rewrite Z.mul_assoc.
   rewrite Z_mod_mult; auto with zarith.
   autorewrite with w_rewrite rm10.
   rewrite Zmod_mod; auto with zarith.
  rewrite spec_ww_compare.
    case Z.compare_spec; rewrite spec_ww_zdigits;
                     rewrite spec_zdigits; intros H2.
  replace (2^[[p]]) with wwB.
    rewrite Zmod_small; auto with zarith.
  unfold base; rewrite H2.
  rewrite spec_ww_digits; auto.
  assert (HH0: [|low (ww_sub p (w_0W w_zdigits))|] =
         [[p]] - Zpos w_digits).
    rewrite spec_low.
    rewrite spec_ww_sub.
    rewrite spec_w_0W; rewrite spec_zdigits.
    rewrite <- Zmod_div_mod; auto with zarith.
    rewrite Zmod_small; auto with zarith.
    split; auto with zarith.
    apply Z.lt_le_trans with (Zpos w_digits); auto with zarith.
    unfold base; apply Zpower2_le_lin; auto with zarith.
    exists wB; unfold base; rewrite <- Zpower_exp; auto with zarith.
    rewrite spec_ww_digits;
      apply f_equal with (f := Z.pow 2); rewrite Pos2Z.inj_xO; auto with zarith.
   simpl ww_to_Z; autorewrite with w_rewrite.
   rewrite spec_pos_mod; rewrite HH0.
   pattern [|xh|] at 2;
     rewrite Z_div_mod_eq with (b := 2 ^ ([[p]] - Zpos w_digits));
     auto with zarith.
   rewrite (fun x => (Z.mul_comm (2 ^ x))); rewrite Z.mul_add_distr_r.
   unfold base; rewrite <- Z.mul_assoc; rewrite <- Zpower_exp;
    auto with zarith.
   rewrite F0; auto with zarith.
   rewrite <- Z.add_assoc; rewrite Zplus_mod; auto with zarith.
   rewrite Z_mod_mult; auto with zarith.
   autorewrite with rm10.
   rewrite Zmod_mod; auto with zarith.
   symmetry; apply Zmod_small; auto with zarith.
   case (spec_to_Z xh); intros U1 U2.
   case (spec_to_Z xl); intros U3 U4.
   split; auto with zarith.
   apply Z.add_nonneg_nonneg; auto with zarith.
   apply Z.mul_nonneg_nonneg; auto with zarith.
   match goal with |- 0 <= ?X mod ?Y =>
    case (Z_mod_lt X Y); auto with zarith
   end.
   match goal with |- ?X mod ?Y * ?U + ?Z < ?T =>
    apply Z.le_lt_trans with ((Y - 1) * U + Z );
     [case (Z_mod_lt X Y); auto with zarith | idtac]
   end.
   match goal with |- ?X * ?U + ?Y < ?Z =>
    apply Z.le_lt_trans with (X * U + (U - 1))
   end.
   apply Z.add_le_mono_l; auto with zarith.
   case (spec_to_Z xl); unfold base; auto with zarith.
   rewrite Z.mul_sub_distr_r; rewrite <- Zpower_exp; auto with zarith.
   rewrite F0; auto with zarith.
  rewrite Zmod_small; auto with zarith.
  case (spec_to_w_Z (WW xh xl)); intros U1 U2.
  split; auto with zarith.
  apply Z.lt_le_trans with (1:= U2).
  unfold base; rewrite spec_ww_digits.
  apply Zpower_le_monotone; auto with zarith.
  split; auto with zarith.
  rewrite Pos2Z.inj_xO; auto with zarith.
 Qed.

End POS_MOD.

Section DoubleDiv32.

 Variable w             : Type.
 Variable w_0           : w.
 Variable w_Bm1         : w.
 Variable w_Bm2         : w.
 Variable w_WW          : w -> w -> zn2z w.
 Variable w_compare     : w -> w -> comparison.
 Variable w_add_c       : w -> w -> carry w.
 Variable w_add_carry_c : w -> w -> carry w.
 Variable w_add         : w -> w -> w.
 Variable w_add_carry   : w -> w -> w.
 Variable w_pred        : w -> w.
 Variable w_sub         : w -> w -> w.
 Variable w_mul_c       : w -> w -> zn2z w.
 Variable w_div21       : w -> w -> w -> w*w.
 Variable ww_sub_c      : zn2z w -> zn2z w -> carry (zn2z w).

 Definition w_div32 a1 a2 a3 b1 b2 :=
  Eval lazy beta iota delta [ww_add_c_cont ww_add] in
  match w_compare a1 b1 with
  | Lt =>
    let (q,r) := w_div21 a1 a2 b1 in
    match ww_sub_c (w_WW r a3) (w_mul_c q b2) with
    | C0 r1 => (q,r1)
    | C1 r1 =>
      let q := w_pred q in
      ww_add_c_cont w_WW w_add_c w_add_carry_c
      (fun r2=>(w_pred q, ww_add w_add_c w_add w_add_carry r2 (WW b1 b2)))
      (fun r2 => (q,r2))
      r1 (WW b1 b2)
    end
  | Eq =>
    ww_add_c_cont w_WW w_add_c w_add_carry_c
    (fun r => (w_Bm2, ww_add w_add_c w_add w_add_carry r (WW b1 b2)))
    (fun r => (w_Bm1,r))
    (WW (w_sub a2 b2) a3) (WW b1 b2)
  | Gt => (w_0, W0) (* cas absurde *)
  end.

 (* Proof *)

  Variable w_digits      : positive.
  Variable w_to_Z : w -> Z.

  Notation wB  := (base w_digits).
  Notation wwB := (base (ww_digits w_digits)).
  Notation "[| x |]" := (w_to_Z x)  (at level 0, x at level 99).
  Notation "[+| c |]" :=
   (interp_carry 1 wB w_to_Z c) (at level 0, x at level 99).
  Notation "[-| c |]" :=
   (interp_carry (-1) wB w_to_Z c) (at level 0, x at level 99).

  Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99).
  Notation "[-[ c ]]" :=
   (interp_carry (-1) wwB (ww_to_Z w_digits w_to_Z) c)
   (at level 0, x at level 99).


  Variable spec_w_0   : [|w_0|] = 0.
  Variable spec_w_Bm1   : [|w_Bm1|] = wB - 1.
  Variable spec_w_Bm2   : [|w_Bm2|] = wB - 2.

  Variable spec_to_Z  : forall x, 0 <= [|x|] < wB.

  Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|].
  Variable spec_compare :
     forall x y, w_compare x y = Z.compare [|x|] [|y|].
  Variable spec_w_add_c  : forall x y, [+|w_add_c x y|] = [|x|] + [|y|].
  Variable spec_w_add_carry_c :
         forall x y, [+|w_add_carry_c x y|] = [|x|] + [|y|] + 1.

  Variable spec_w_add : forall x y, [|w_add x y|] = ([|x|] + [|y|]) mod wB.
  Variable spec_w_add_carry :
	 forall x y, [|w_add_carry x y|] = ([|x|] + [|y|] + 1) mod wB.

  Variable spec_pred : forall x, [|w_pred x|] = ([|x|] - 1) mod wB.
  Variable spec_sub : forall x y, [|w_sub x y|] = ([|x|] - [|y|]) mod wB.

  Variable spec_mul_c : forall x y, [[ w_mul_c x y ]] = [|x|] * [|y|].
  Variable spec_div21 : forall a1 a2 b,
      wB/2 <= [|b|] ->
      [|a1|] < [|b|] ->
      let (q,r) := w_div21 a1 a2 b in
      [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\
      0 <= [|r|] < [|b|].

  Variable spec_ww_sub_c : forall x y, [-[ww_sub_c x y]] = [[x]] - [[y]].

  Ltac Spec_w_to_Z x :=
   let H:= fresh "HH" in
   assert (H:= spec_to_Z x).
  Ltac Spec_ww_to_Z x :=
   let H:= fresh "HH" in
   assert (H:= spec_ww_to_Z w_digits w_to_Z spec_to_Z x).

  Theorem wB_div2: forall x, wB/2  <= x -> wB <= 2 * x.
   intros x H; rewrite <- wB_div_2; apply Z.mul_le_mono_nonneg_l; auto with zarith.
  Qed.

  Lemma Zmult_lt_0_reg_r_2 : forall n m : Z, 0 <= n -> 0 < m * n -> 0 < m.
  Proof.
   intros n m H1 H2;apply Z.mul_pos_cancel_r with n;trivial.
   Z.le_elim H1; trivial.
   subst;rewrite Z.mul_0_r in H2;discriminate H2.
  Qed.

  Theorem spec_w_div32 : forall a1 a2 a3 b1 b2,
     wB/2 <= [|b1|] ->
     [[WW a1 a2]] < [[WW b1 b2]] ->
     let (q,r) := w_div32 a1 a2 a3 b1 b2 in
     [|a1|] * wwB + [|a2|] * wB  + [|a3|] =
        [|q|] *  ([|b1|] * wB + [|b2|])  + [[r]] /\
     0 <= [[r]] < [|b1|] * wB + [|b2|].
  Proof.
   intros a1 a2 a3 b1 b2 Hle Hlt.
   assert (U:= lt_0_wB w_digits); assert (U1:= lt_0_wwB w_digits).
   Spec_w_to_Z a1;Spec_w_to_Z a2;Spec_w_to_Z a3;Spec_w_to_Z b1;Spec_w_to_Z b2.
   rewrite wwB_wBwB; rewrite Z.pow_2_r; rewrite Z.mul_assoc;rewrite <- Z.mul_add_distr_r.
   change (w_div32 a1 a2 a3 b1 b2) with
    match w_compare a1 b1 with
    | Lt =>
     let (q,r) := w_div21 a1 a2 b1 in
     match ww_sub_c (w_WW r a3) (w_mul_c q b2) with
     | C0 r1 => (q,r1)
     | C1 r1 =>
      let q := w_pred q in
      ww_add_c_cont w_WW w_add_c w_add_carry_c
      (fun r2=>(w_pred q, ww_add w_add_c w_add w_add_carry r2 (WW b1 b2)))
      (fun r2 => (q,r2))
      r1 (WW b1 b2)
     end
    | Eq =>
     ww_add_c_cont w_WW w_add_c w_add_carry_c
     (fun r => (w_Bm2, ww_add w_add_c w_add w_add_carry r (WW b1 b2)))
     (fun r => (w_Bm1,r))
     (WW (w_sub a2 b2) a3) (WW b1 b2)
    | Gt => (w_0, W0) (* cas absurde *)
    end.
   rewrite spec_compare. case Z.compare_spec; intro Hcmp.
   simpl in Hlt.
   rewrite Hcmp in Hlt;assert ([|a2|] < [|b2|]). omega.
   assert ([[WW (w_sub a2 b2) a3]] = ([|a2|]-[|b2|])*wB + [|a3|] + wwB).
    simpl;rewrite spec_sub.
    assert ([|a2|] - [|b2|] = wB*(-1) + ([|a2|] - [|b2|] + wB)). ring.
    assert (0 <= [|a2|] - [|b2|] + wB < wB). omega.
    rewrite <-(Zmod_unique ([|a2|]-[|b2|]) wB (-1) ([|a2|]-[|b2|]+wB) H1 H0).
    rewrite wwB_wBwB;ring.
   assert (U2 := wB_pos w_digits).
   eapply spec_ww_add_c_cont with (P :=
     fun (x y:zn2z w) (res:w*zn2z w) =>
     let (q, r) := res in
     ([|a1|] * wB + [|a2|]) * wB + [|a3|] =
     [|q|] * ([|b1|] * wB + [|b2|]) + [[r]] /\
     0 <= [[r]] < [|b1|] * wB + [|b2|]);eauto.
   rewrite H0;intros r.
   repeat
    (rewrite spec_ww_add;eauto || rewrite spec_w_Bm1 || rewrite spec_w_Bm2);
   simpl ww_to_Z;try rewrite Z.mul_1_l;intros H1.
   assert (0<= ([[r]] + ([|b1|] * wB + [|b2|])) - wwB < [|b1|] * wB + [|b2|]).
   Spec_ww_to_Z r;split;zarith.
   rewrite H1.
   assert (H12:= wB_div2 Hle). assert (wwB <= 2 * [|b1|] * wB).
   rewrite wwB_wBwB; rewrite Z.pow_2_r; zarith.
   assert (-wwB < ([|a2|] - [|b2|]) * wB + [|a3|] < 0).
   split. apply Z.lt_le_trans with (([|a2|] - [|b2|]) * wB);zarith.
   rewrite wwB_wBwB;replace (-(wB^2)) with (-wB*wB);[zarith | ring].
   apply Z.mul_lt_mono_pos_r;zarith.
   apply Z.le_lt_trans with (([|a2|] - [|b2|]) * wB + (wB -1));zarith.
   replace ( ([|a2|] - [|b2|]) * wB + (wB - 1)) with
     (([|a2|] - [|b2|] + 1) * wB + - 1);[zarith | ring].
   assert (([|a2|] - [|b2|] + 1) * wB <= 0);zarith.
   replace 0 with (0*wB);zarith.
   replace (([|a2|] - [|b2|]) * wB + [|a3|] + wwB + ([|b1|] * wB + [|b2|]) +
              ([|b1|] * wB + [|b2|]) - wwB) with
         (([|a2|] - [|b2|]) * wB + [|a3|] + 2*[|b1|] * wB + 2*[|b2|]);
   [zarith | ring].
   rewrite <- (Zmod_unique ([[r]] + ([|b1|] * wB + [|b2|])) wwB
             1 ([[r]] + ([|b1|] * wB + [|b2|]) - wwB));zarith;try (ring;fail).
   split. rewrite H1;rewrite Hcmp;ring. trivial.
   Spec_ww_to_Z (WW b1 b2). simpl in HH4;zarith.
   rewrite H0;intros r;repeat
    (rewrite spec_w_Bm1 || rewrite spec_w_Bm2);
   simpl ww_to_Z;try rewrite Z.mul_1_l;intros H1.
   assert ([[r]]=([|a2|]-[|b2|])*wB+[|a3|]+([|b1|]*wB+[|b2|])). zarith.
   split. rewrite H2;rewrite Hcmp;ring.
   split. Spec_ww_to_Z r;zarith.
   rewrite H2.
   assert (([|a2|] - [|b2|]) * wB + [|a3|] < 0);zarith.
   apply Z.le_lt_trans with (([|a2|] - [|b2|]) * wB + (wB -1));zarith.
   replace ( ([|a2|] - [|b2|]) * wB + (wB - 1)) with
     (([|a2|] - [|b2|] + 1) * wB + - 1);[zarith|ring].
   assert (([|a2|] - [|b2|] + 1) * wB <= 0);zarith.
   replace 0 with (0*wB);zarith.
   (* Cas Lt *)
   assert (Hdiv21 := spec_div21 a2 Hle Hcmp);
    destruct (w_div21 a1 a2 b1) as (q, r);destruct Hdiv21.
   rewrite H.
   assert (Hq := spec_to_Z q).
   generalize
    (spec_ww_sub_c (w_WW r a3) (w_mul_c q b2));
    destruct (ww_sub_c (w_WW r a3) (w_mul_c q b2))
    as [r1|r1];repeat (rewrite spec_w_WW || rewrite spec_mul_c);
    unfold interp_carry;intros H1.
    rewrite H1.
   split. ring. split.
   rewrite <- H1;destruct (spec_ww_to_Z w_digits w_to_Z spec_to_Z r1);trivial.
   apply Z.le_lt_trans with ([|r|] * wB + [|a3|]).
   assert ( 0 <= [|q|] * [|b2|]);zarith.
   apply beta_lex_inv;zarith.
   assert ([[r1]] = [|r|] * wB + [|a3|] - [|q|] * [|b2|] + wwB).
   rewrite <- H1;ring.
   Spec_ww_to_Z r1; assert (0 <= [|r|]*wB). zarith.
   assert (0 < [|q|] * [|b2|]). zarith.
   assert (0 < [|q|]).
    apply Zmult_lt_0_reg_r_2 with [|b2|];zarith.
   eapply spec_ww_add_c_cont with (P :=
     fun (x y:zn2z w) (res:w*zn2z w) =>
     let (q0, r0) := res in
      ([|q|] * [|b1|] + [|r|]) * wB + [|a3|] =
      [|q0|] * ([|b1|] * wB + [|b2|]) + [[r0]] /\
      0 <= [[r0]] < [|b1|] * wB + [|b2|]);eauto.
   intros r2;repeat (rewrite spec_pred || rewrite spec_ww_add;eauto);
   simpl ww_to_Z;intros H7.
   assert (0 < [|q|] - 1).
   assert (H6 : 1 <= [|q|]) by zarith.
   Z.le_elim H6;zarith.
   rewrite <- H6 in H2;rewrite H2 in H7.
   assert (0 < [|b1|]*wB). apply Z.mul_pos_pos;zarith.
   Spec_ww_to_Z r2. zarith.
   rewrite (Zmod_small ([|q|] -1));zarith.
   rewrite (Zmod_small ([|q|] -1 -1));zarith.
   assert ([[r2]] + ([|b1|] * wB + [|b2|]) =
       wwB * 1 +
       ([|r|] * wB + [|a3|] - [|q|] * [|b2|] + 2 * ([|b1|] * wB + [|b2|]))).
   rewrite H7;rewrite H2;ring.
   assert
    ([|r|]*wB + [|a3|] - [|q|]*[|b2|] + 2 * ([|b1|]*wB + [|b2|])
        < [|b1|]*wB + [|b2|]).
   Spec_ww_to_Z r2;omega.
   Spec_ww_to_Z (WW b1 b2). simpl in HH5.
   assert
    (0 <= [|r|]*wB + [|a3|] - [|q|]*[|b2|] + 2 * ([|b1|]*wB + [|b2|])
       < wwB). split;try omega.
   replace (2*([|b1|]*wB+[|b2|])) with ((2*[|b1|])*wB+2*[|b2|]). 2:ring.
   assert (H12:= wB_div2 Hle). assert (wwB <= 2 * [|b1|] * wB).
   rewrite wwB_wBwB; rewrite Z.pow_2_r; zarith. omega.
   rewrite <- (Zmod_unique
            ([[r2]] + ([|b1|] * wB + [|b2|]))
            wwB
            1
            ([|r|] * wB + [|a3|] - [|q|] * [|b2|] + 2*([|b1|] * wB + [|b2|]))
            H10 H8).
   split. ring. zarith.
   intros r2;repeat (rewrite spec_pred);simpl ww_to_Z;intros H7.
   rewrite (Zmod_small ([|q|] -1));zarith.
   split.
   replace [[r2]] with  ([[r1]] + ([|b1|] * wB + [|b2|]) -wwB).
   rewrite H2; ring. rewrite <- H7; ring.
   Spec_ww_to_Z r2;Spec_ww_to_Z r1. omega.
   simpl in Hlt.
   assert ([|a1|] * wB + [|a2|] <= [|b1|] * wB + [|b2|]). zarith.
   assert (H1 := beta_lex _ _ _ _ _ H HH0 HH3). rewrite spec_w_0;simpl;zarith.
  Qed.


End DoubleDiv32.

Section DoubleDiv21.
 Variable w : Type.
 Variable w_0 : w.

 Variable w_0W : w -> zn2z w.
 Variable w_div32 : w -> w -> w -> w -> w -> w * zn2z w.

 Variable ww_1 : zn2z w.
 Variable ww_compare : zn2z w -> zn2z w -> comparison.
 Variable ww_sub : zn2z w -> zn2z w -> zn2z w.


 Definition ww_div21 a1 a2 b :=
  match a1 with
  | W0 =>
    match ww_compare a2 b with
    | Gt => (ww_1, ww_sub a2 b)
    | Eq => (ww_1, W0)
    | Lt => (W0, a2)
    end
  | WW a1h a1l =>
    match a2 with
    | W0 =>
      match b with
      | W0 => (W0,W0) (* cas absurde *)
      | WW b1 b2 =>
        let (q1, r)  := w_div32 a1h a1l w_0 b1 b2 in
        match r with
        | W0 => (WW q1 w_0, W0)
        | WW r1 r2 =>
	  let (q2, s)  := w_div32 r1 r2 w_0 b1 b2 in
          (WW q1 q2, s)
        end
      end
    | WW a2h a2l =>
      match b with
      | W0 => (W0,W0) (* cas absurde *)
      | WW b1 b2 =>
        let (q1, r)  := w_div32 a1h a1l a2h b1 b2 in
        match r with
        | W0 => (WW q1 w_0, w_0W a2l)
        | WW r1 r2 =>
	  let (q2, s)  := w_div32 r1 r2 a2l b1 b2 in
          (WW q1 q2, s)
        end
      end
    end
  end.

 (* Proof *)

  Variable w_digits : positive.
  Variable w_to_Z : w -> Z.
  Notation wB  := (base w_digits).
  Notation wwB := (base (ww_digits w_digits)).
  Notation "[| x |]" := (w_to_Z x)  (at level 0, x at level 99).
  Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99).
  Notation "[-[ c ]]" :=
   (interp_carry (-1) wwB (ww_to_Z w_digits w_to_Z) c)
   (at level 0, x at level 99).

  Variable spec_w_0   : [|w_0|] = 0.
  Variable spec_to_Z  : forall x, 0 <= [|x|] < wB.
  Variable spec_w_0W : forall l, [[w_0W l]] = [|l|].
  Variable spec_w_div32 : forall a1 a2 a3 b1 b2,
     wB/2 <= [|b1|] ->
     [[WW a1 a2]] < [[WW b1 b2]] ->
     let (q,r) := w_div32 a1 a2 a3 b1 b2 in
     [|a1|] * wwB + [|a2|] * wB  + [|a3|] =
        [|q|] *  ([|b1|] * wB + [|b2|])  + [[r]] /\
     0 <= [[r]] < [|b1|] * wB + [|b2|].
  Variable spec_ww_1 : [[ww_1]] = 1.
  Variable spec_ww_compare :  forall x y,
    ww_compare x y = Z.compare [[x]] [[y]].
  Variable spec_ww_sub : forall x y, [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB.

  Theorem wwB_div: wwB  = 2 * (wwB / 2).
  Proof.
   rewrite wwB_div_2; rewrite  Z.mul_assoc; rewrite  wB_div_2; auto.
   rewrite <- Z.pow_2_r; apply wwB_wBwB.
  Qed.

  Ltac Spec_w_to_Z x :=
   let H:= fresh "HH" in
   assert (H:= spec_to_Z x).
  Ltac Spec_ww_to_Z x :=
   let H:= fresh "HH" in
   assert (H:= spec_ww_to_Z w_digits w_to_Z spec_to_Z x).

  Theorem   spec_ww_div21 : forall a1 a2 b,
     wwB/2 <= [[b]] ->
     [[a1]] < [[b]] ->
     let (q,r) := ww_div21 a1 a2 b in
     [[a1]] *wwB+[[a2]] = [[q]] *  [[b]] + [[r]] /\ 0 <= [[r]] < [[b]].
  Proof.
   assert (U:= lt_0_wB w_digits).
   assert (U1:= lt_0_wwB w_digits).
   intros a1 a2 b H Hlt; unfold ww_div21.
   Spec_ww_to_Z b; assert (Eq: 0 < [[b]]).    Spec_ww_to_Z a1;omega.
   generalize Hlt H ;clear Hlt H;case a1.
   intros H1 H2;simpl in H1;Spec_ww_to_Z a2.
   rewrite spec_ww_compare. case Z.compare_spec;
   simpl;try rewrite spec_ww_1;autorewrite with rm10; intros;zarith.
   rewrite spec_ww_sub;simpl. rewrite Zmod_small;zarith.
   split. ring.
   assert (wwB <= 2*[[b]]);zarith.
   rewrite wwB_div;zarith.
   intros a1h a1l.  Spec_w_to_Z a1h;Spec_w_to_Z a1l. Spec_ww_to_Z a2.
   destruct a2 as [ |a3 a4];
    (destruct b as [ |b1 b2];[unfold Z.le in Eq;discriminate Eq|idtac]);
   try (Spec_w_to_Z a3; Spec_w_to_Z a4); Spec_w_to_Z b1; Spec_w_to_Z b2;
   intros Hlt H;  match goal with |-context [w_div32 ?X ?Y ?Z ?T ?U] =>
     generalize (@spec_w_div32 X Y Z T U); case (w_div32 X Y Z T U);
     intros q1 r H0
   end; (assert (Eq1: wB / 2 <= [|b1|]);[
    apply (@beta_lex (wB / 2) 0 [|b1|] [|b2|] wB); auto with zarith;
    autorewrite with rm10;repeat rewrite (Z.mul_comm wB);
    rewrite <- wwB_div_2; trivial
   | generalize (H0 Eq1 Hlt);clear H0;destruct r as [ |r1 r2];simpl;
     try rewrite spec_w_0; try rewrite spec_w_0W;repeat rewrite Z.add_0_r;
     intros (H1,H2) ]).
   split;[rewrite wwB_wBwB; rewrite Z.pow_2_r | trivial].
   rewrite Z.mul_assoc;rewrite Z.mul_add_distr_r;rewrite <- Z.mul_assoc;
   rewrite <- Z.pow_2_r; rewrite <- wwB_wBwB;rewrite H1;ring.
   destruct H2 as (H2,H3);match goal with |-context [w_div32 ?X ?Y ?Z ?T ?U] =>
     generalize (@spec_w_div32 X Y Z T U); case (w_div32 X Y Z T U);
     intros q r H0;generalize (H0 Eq1 H3);clear H0;intros (H4,H5) end.
   split;[rewrite wwB_wBwB | trivial].
   rewrite Z.pow_2_r.
   rewrite Z.mul_assoc;rewrite Z.mul_add_distr_r;rewrite <- Z.mul_assoc;
   rewrite <- Z.pow_2_r.
   rewrite <- wwB_wBwB;rewrite H1.
   rewrite spec_w_0 in H4;rewrite Z.add_0_r in H4.
   repeat rewrite Z.mul_add_distr_r. rewrite <- (Z.mul_assoc [|r1|]).
   rewrite <- Z.pow_2_r; rewrite <- wwB_wBwB;rewrite H4;simpl;ring.
   split;[rewrite wwB_wBwB | split;zarith].
   replace (([|a1h|] * wB + [|a1l|]) * wB^2 + ([|a3|] * wB + [|a4|]))
   with (([|a1h|] * wwB + [|a1l|] * wB + [|a3|])*wB+ [|a4|]).
   rewrite H1;ring. rewrite wwB_wBwB;ring.
   change [|a4|] with (0*wB+[|a4|]);apply beta_lex_inv;zarith.
   assert (1 <= wB/2);zarith.
    assert (H_:= wB_pos w_digits);apply Zdiv_le_lower_bound;zarith.
   destruct H2 as (H2,H3);match goal with |-context [w_div32 ?X ?Y ?Z ?T ?U] =>
     generalize (@spec_w_div32 X Y Z T U); case (w_div32 X Y Z T U);
     intros q r H0;generalize (H0 Eq1 H3);clear H0;intros (H4,H5) end.
   split;trivial.
   replace (([|a1h|] * wB + [|a1l|]) * wwB + ([|a3|] * wB + [|a4|])) with
   (([|a1h|] * wwB + [|a1l|] * wB + [|a3|])*wB + [|a4|]);
   [rewrite H1 | rewrite wwB_wBwB;ring].
   replace (([|q1|]*([|b1|]*wB+[|b2|])+([|r1|]*wB+[|r2|]))*wB+[|a4|]) with
   (([|q1|]*([|b1|]*wB+[|b2|]))*wB+([|r1|]*wwB+[|r2|]*wB+[|a4|]));
   [rewrite H4;simpl|rewrite wwB_wBwB];ring.
  Qed.

End DoubleDiv21.

Section DoubleDivGt.
 Variable w : Type.
 Variable w_digits : positive.
 Variable w_0 : w.

 Variable w_WW : w -> w -> zn2z w.
 Variable w_0W : w -> zn2z w.
 Variable w_compare : w -> w -> comparison.
 Variable w_eq0 : w -> bool.
 Variable w_opp_c : w -> carry w.
 Variable w_opp w_opp_carry : w -> w.
 Variable w_sub_c : w -> w -> carry w.
 Variable w_sub w_sub_carry : w -> w -> w.

 Variable w_div_gt : w -> w -> w*w.
 Variable w_mod_gt : w -> w -> w.
 Variable w_gcd_gt : w -> w -> w.
 Variable w_add_mul_div : w -> w -> w -> w.
 Variable w_head0 : w -> w.
 Variable w_div21 : w -> w -> w -> w * w.
 Variable w_div32 : w -> w -> w -> w -> w -> w * zn2z w.


 Variable _ww_zdigits : zn2z w.
 Variable ww_1 : zn2z w.
 Variable ww_add_mul_div : zn2z w -> zn2z w -> zn2z w -> zn2z w.

 Variable w_zdigits : w.

 Definition ww_div_gt_aux ah al bh bl :=
  Eval lazy beta iota delta [ww_sub ww_opp] in
    let p := w_head0 bh in
    match w_compare p w_0 with
    | Gt =>
      let b1 := w_add_mul_div p bh bl in
      let b2 := w_add_mul_div p bl w_0 in
      let a1 := w_add_mul_div p w_0 ah in
      let a2 := w_add_mul_div p ah al in
      let a3 := w_add_mul_div p al w_0 in
      let (q,r) := w_div32 a1 a2 a3 b1 b2 in
      (WW w_0 q, ww_add_mul_div
        (ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c
            w_opp w_sub w_sub_carry _ww_zdigits (w_0W p)) W0 r)
    | _ => (ww_1, ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c
            w_opp w_sub w_sub_carry (WW ah al) (WW bh bl))
    end.

 Definition ww_div_gt a b :=
  Eval lazy beta iota delta [ww_div_gt_aux double_divn1
  double_divn1_p double_divn1_p_aux double_divn1_0 double_divn1_0_aux
  double_split double_0 double_WW] in
  match a, b with
  | W0, _ => (W0,W0)
  | _, W0 => (W0,W0)
  | WW ah al, WW bh bl =>
    if w_eq0 ah then
     let (q,r) := w_div_gt al bl in
     (WW w_0 q, w_0W r)
    else
     match w_compare w_0 bh with
     | Eq =>
       let(q,r):=
        double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21
                  w_compare w_sub 1 a bl in
       (q, w_0W r)
     | Lt => ww_div_gt_aux ah al bh bl
     | Gt => (W0,W0) (* cas absurde *)
     end
  end.

 Definition ww_mod_gt_aux ah al bh bl :=
  Eval lazy beta iota delta [ww_sub ww_opp] in
    let p := w_head0 bh in
    match w_compare p w_0 with
    | Gt =>
      let b1 := w_add_mul_div p bh bl in
      let b2 := w_add_mul_div p bl w_0 in
      let a1 := w_add_mul_div p w_0 ah in
      let a2 := w_add_mul_div p ah al in
      let a3 := w_add_mul_div p al w_0 in
      let (q,r) := w_div32 a1 a2 a3 b1 b2 in
      ww_add_mul_div (ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c
         w_opp w_sub w_sub_carry _ww_zdigits (w_0W p)) W0 r
    | _ =>
      ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c
         w_opp w_sub w_sub_carry (WW ah al) (WW bh bl)
    end.

 Definition ww_mod_gt a b :=
  Eval lazy beta iota delta [ww_mod_gt_aux double_modn1
  double_modn1_p double_modn1_p_aux double_modn1_0 double_modn1_0_aux
  double_split double_0 double_WW snd] in
  match a, b with
  | W0, _ => W0
  | _, W0 => W0
  | WW ah al, WW bh bl =>
    if w_eq0 ah then w_0W (w_mod_gt al bl)
    else
     match w_compare w_0 bh with
     | Eq =>
       w_0W (double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21
             w_compare w_sub 1 a bl)
     | Lt => ww_mod_gt_aux ah al bh bl
     | Gt => W0 (* cas absurde *)
     end
  end.

  Definition ww_gcd_gt_body (cont: w->w->w->w->zn2z w) (ah al bh bl: w) :=
   Eval lazy beta iota delta [ww_mod_gt_aux double_modn1
   double_modn1_p double_modn1_p_aux double_modn1_0 double_modn1_0_aux
   double_split double_0 double_WW snd] in
    match w_compare w_0 bh with
    | Eq =>
      match w_compare w_0 bl with
      | Eq => WW ah al (* normalement n'arrive pas si forme normale *)
      | Lt =>
	let m := double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21
                   w_compare w_sub 1 (WW ah al) bl in
        WW w_0 (w_gcd_gt bl m)
      | Gt => W0 (* absurde *)
      end
    | Lt =>
      let m := ww_mod_gt_aux ah al bh bl in
      match m with
      | W0 => WW bh bl
      | WW mh ml =>
        match w_compare w_0 mh with
        | Eq =>
          match w_compare w_0 ml with
          | Eq => WW bh bl
          | _  =>
            let r := double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21
                      w_compare w_sub 1 (WW bh bl) ml in
            WW w_0 (w_gcd_gt ml r)
          end
        | Lt =>
          let r := ww_mod_gt_aux bh bl mh ml in
          match r with
          | W0 => m
          | WW rh rl => cont mh ml rh rl
          end
        | Gt => W0 (* absurde *)
        end
      end
    | Gt => W0 (* absurde *)
    end.

  Fixpoint ww_gcd_gt_aux
     (p:positive) (cont: w -> w -> w -> w -> zn2z w) (ah al bh bl : w)
        {struct p} : zn2z w :=
    ww_gcd_gt_body
       (fun mh ml rh rl => match p with
        | xH => cont mh ml rh rl
        | xO p => ww_gcd_gt_aux p (ww_gcd_gt_aux p cont) mh ml rh rl
        | xI p => ww_gcd_gt_aux p (ww_gcd_gt_aux p cont) mh ml rh rl
        end) ah al bh bl.


  (* Proof *)

  Variable w_to_Z : w -> Z.
  Notation wB  := (base w_digits).
  Notation wwB := (base (ww_digits w_digits)).
  Notation "[| x |]" := (w_to_Z x)  (at level 0, x at level 99).
  Notation "[-| c |]" :=
   (interp_carry (-1) wB w_to_Z c) (at level 0, x at level 99).

  Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99).

  Variable spec_w_0   : [|w_0|] = 0.
  Variable spec_to_Z  : forall x, 0 <= [|x|] < wB.
  Variable spec_to_w_Z  : forall x, 0 <= [[x]] < wwB.

  Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|].
  Variable spec_w_0W : forall l, [[w_0W l]] = [|l|].
  Variable spec_compare :
     forall x y, w_compare x y = Z.compare [|x|] [|y|].
  Variable spec_eq0 : forall x, w_eq0 x = true -> [|x|] = 0.

  Variable spec_opp_c : forall x, [-|w_opp_c x|] = -[|x|].
  Variable spec_opp : forall x, [|w_opp x|] = (-[|x|]) mod wB.
  Variable spec_opp_carry : forall x, [|w_opp_carry x|] = wB - [|x|] - 1.

  Variable spec_sub_c : forall x y, [-|w_sub_c x y|] = [|x|] - [|y|].
  Variable spec_sub : forall x y, [|w_sub x y|] = ([|x|] - [|y|]) mod wB.
  Variable spec_sub_carry :
	 forall x y, [|w_sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB.

  Variable spec_div_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
      let (q,r) := w_div_gt a b in
      [|a|] = [|q|] * [|b|] + [|r|] /\
      0 <= [|r|] < [|b|].
  Variable spec_mod_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
      [|w_mod_gt a b|] = [|a|] mod [|b|].
  Variable spec_gcd_gt : forall a b, [|a|] > [|b|] ->
      Zis_gcd [|a|] [|b|] [|w_gcd_gt a b|].

  Variable spec_add_mul_div : forall x y p,
       [|p|] <= Zpos w_digits ->
       [| w_add_mul_div p x y |] =
         ([|x|] * (2 ^ ([|p|])) +
          [|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB.
  Variable spec_head0  : forall x,  0 < [|x|] ->
	 wB/ 2 <= 2 ^ [|w_head0 x|] * [|x|] < wB.

  Variable spec_div21 : forall a1 a2 b,
      wB/2 <= [|b|] ->
      [|a1|] < [|b|] ->
      let (q,r) := w_div21 a1 a2 b in
      [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\
      0 <= [|r|] < [|b|].

  Variable spec_w_div32 : forall a1 a2 a3 b1 b2,
     wB/2 <= [|b1|] ->
     [[WW a1 a2]] < [[WW b1 b2]] ->
     let (q,r) := w_div32 a1 a2 a3 b1 b2 in
     [|a1|] * wwB + [|a2|] * wB  + [|a3|] =
        [|q|] *  ([|b1|] * wB + [|b2|])  + [[r]] /\
     0 <= [[r]] < [|b1|] * wB + [|b2|].

  Variable spec_w_zdigits: [|w_zdigits|] = Zpos w_digits.

  Variable spec_ww_digits_ : [[_ww_zdigits]] = Zpos (xO w_digits).
  Variable spec_ww_1 : [[ww_1]] = 1.
  Variable spec_ww_add_mul_div : forall x y p,
       [[p]] <= Zpos (xO w_digits) ->
       [[ ww_add_mul_div p x y ]] =
         ([[x]] * (2^[[p]]) +
          [[y]] / (2^(Zpos (xO w_digits) - [[p]]))) mod wwB.

  Ltac Spec_w_to_Z x :=
   let H:= fresh "HH" in
   assert (H:= spec_to_Z x).

  Ltac Spec_ww_to_Z x :=
   let H:= fresh "HH" in
   assert (H:= spec_ww_to_Z w_digits w_to_Z spec_to_Z x).

  Lemma to_Z_div_minus_p : forall x p,
   0 < [|p|] < Zpos w_digits  ->
   0 <= [|x|] / 2 ^ (Zpos w_digits - [|p|]) < 2 ^ [|p|].
  Proof.
   intros x p H;Spec_w_to_Z x.
   split. apply Zdiv_le_lower_bound;zarith.
   apply Zdiv_lt_upper_bound;zarith.
   rewrite <- Zpower_exp;zarith.
   ring_simplify ([|p|] + (Zpos w_digits - [|p|])); unfold base in HH;zarith.
  Qed.
  Hint Resolve to_Z_div_minus_p : zarith.

  Lemma spec_ww_div_gt_aux : forall ah al bh bl,
      [[WW ah al]] > [[WW bh bl]] ->
      0 < [|bh|] ->
      let (q,r) := ww_div_gt_aux ah al bh bl in
      [[WW ah al]] = [[q]] * [[WW bh bl]] + [[r]] /\
      0 <= [[r]] < [[WW bh bl]].
  Proof.
   intros ah al bh bl Hgt Hpos;unfold ww_div_gt_aux.
   change
   (let (q, r) := let p := w_head0 bh in
    match w_compare p w_0 with
    | Gt =>
      let b1 := w_add_mul_div p bh bl in
      let b2 := w_add_mul_div p bl w_0 in
      let a1 := w_add_mul_div p w_0 ah in
      let a2 := w_add_mul_div p ah al in
      let a3 := w_add_mul_div p al w_0 in
      let (q,r) := w_div32 a1 a2 a3 b1 b2 in
      (WW w_0 q, ww_add_mul_div
        (ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c
            w_opp w_sub w_sub_carry _ww_zdigits (w_0W p)) W0 r)
    | _ => (ww_1, ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c
            w_opp w_sub w_sub_carry (WW ah al) (WW bh bl))
    end in [[WW ah al]]=[[q]]*[[WW bh bl]]+[[r]] /\ 0 <=[[r]]< [[WW bh bl]]).
   assert (Hh := spec_head0 Hpos).
   lazy zeta.
   rewrite spec_compare; case Z.compare_spec;
    rewrite spec_w_0; intros HH.
   generalize Hh; rewrite HH; simpl Z.pow;
        rewrite Z.mul_1_l; intros (HH1, HH2); clear HH.
   assert (wwB <= 2*[[WW bh bl]]).
    apply Z.le_trans with (2*[|bh|]*wB).
    rewrite wwB_wBwB; rewrite Z.pow_2_r; apply Z.mul_le_mono_nonneg_r; zarith.
    rewrite <- wB_div_2; apply Z.mul_le_mono_nonneg_l; zarith.
    simpl ww_to_Z;rewrite Z.mul_add_distr_l;rewrite Z.mul_assoc.
    Spec_w_to_Z bl;zarith.
   Spec_ww_to_Z (WW ah al).
   rewrite spec_ww_sub;eauto.
   simpl;rewrite spec_ww_1;rewrite Z.mul_1_l;simpl.
   simpl ww_to_Z in Hgt, H, HH;rewrite Zmod_small;split;zarith.
   case (spec_to_Z (w_head0 bh)); auto with zarith.
   assert ([|w_head0 bh|] < Zpos w_digits).
    destruct (Z_lt_ge_dec [|w_head0 bh|]  (Zpos w_digits));trivial.
    exfalso.
    assert (2 ^ [|w_head0 bh|] * [|bh|] >= wB);auto with zarith.
    apply Z.le_ge; replace wB with (wB * 1);try ring.
    Spec_w_to_Z bh;apply Z.mul_le_mono_nonneg;zarith.
    unfold base;apply Zpower_le_monotone;zarith.
   assert (HHHH : 0 < [|w_head0 bh|] < Zpos w_digits); auto with zarith.
   assert (Hb:= Z.lt_le_incl _ _ H).
   generalize (spec_add_mul_div w_0 ah Hb)
    (spec_add_mul_div ah al Hb)
    (spec_add_mul_div al w_0 Hb)
    (spec_add_mul_div bh bl Hb)
    (spec_add_mul_div bl w_0  Hb);
   rewrite spec_w_0; repeat rewrite Z.mul_0_l;repeat rewrite Z.add_0_l;
   rewrite Zdiv_0_l;repeat rewrite Z.add_0_r.
   Spec_w_to_Z ah;Spec_w_to_Z bh.
   unfold base;repeat rewrite Zmod_shift_r;zarith.
   assert (H3:=to_Z_div_minus_p ah HHHH);assert(H4:=to_Z_div_minus_p al HHHH);
   assert (H5:=to_Z_div_minus_p bl HHHH).
   rewrite Z.mul_comm in Hh.
   assert (2^[|w_head0 bh|] < wB). unfold base;apply Zpower_lt_monotone;zarith.
   unfold base in H0;rewrite Zmod_small;zarith.
   fold wB; rewrite (Zmod_small ([|bh|] * 2 ^ [|w_head0 bh|]));zarith.
   intros U1 U2 U3 V1 V2.
   generalize (@spec_w_div32 (w_add_mul_div (w_head0 bh) w_0 ah)
               (w_add_mul_div (w_head0 bh) ah al)
               (w_add_mul_div (w_head0 bh) al w_0)
               (w_add_mul_div (w_head0 bh) bh bl)
               (w_add_mul_div (w_head0 bh) bl w_0)).
   destruct (w_div32 (w_add_mul_div (w_head0 bh) w_0 ah)
              (w_add_mul_div (w_head0 bh) ah al)
              (w_add_mul_div (w_head0 bh) al w_0)
              (w_add_mul_div (w_head0 bh) bh bl)
              (w_add_mul_div (w_head0 bh) bl w_0)) as (q,r).
   rewrite V1;rewrite V2. rewrite Z.mul_add_distr_r.
   rewrite <- (Z.add_assoc ([|bh|] * 2 ^ [|w_head0 bh|] * wB)).
   unfold base;rewrite <- shift_unshift_mod;zarith. fold wB.
   replace ([|bh|] * 2 ^ [|w_head0 bh|] * wB + [|bl|] * 2 ^ [|w_head0 bh|]) with
    ([[WW bh bl]] * 2^[|w_head0 bh|]). 2:simpl;ring.
   fold wwB. rewrite wwB_wBwB. rewrite Z.pow_2_r. rewrite U1;rewrite U2;rewrite U3.
   rewrite Z.mul_assoc. rewrite Z.mul_add_distr_r.
   rewrite (Z.add_assoc ([|ah|] / 2^(Zpos(w_digits) - [|w_head0 bh|])*wB * wB)).
   rewrite <- Z.mul_add_distr_r.  rewrite <- Z.add_assoc.
   unfold base;repeat rewrite <- shift_unshift_mod;zarith. fold wB.
   replace ([|ah|] * 2 ^ [|w_head0 bh|] * wB + [|al|] * 2 ^ [|w_head0 bh|]) with
    ([[WW ah al]] * 2^[|w_head0 bh|]). 2:simpl;ring.
   intros Hd;destruct Hd;zarith.
   simpl. apply beta_lex_inv;zarith. rewrite U1;rewrite V1.
   assert ([|ah|] / 2 ^ (Zpos (w_digits) - [|w_head0 bh|]) < wB/2);zarith.
   apply Zdiv_lt_upper_bound;zarith.
   unfold base.
   replace (2^Zpos (w_digits)) with (2^(Zpos (w_digits) - 1)*2).
   rewrite Z_div_mult;zarith.  rewrite <- Zpower_exp;zarith.
   apply Z.lt_le_trans with wB;zarith.
   unfold base;apply Zpower_le_monotone;zarith.
   pattern 2 at 2;replace 2 with (2^1);trivial.
   rewrite <- Zpower_exp;zarith. ring_simplify (Zpos (w_digits) - 1 + 1);trivial.
   change [[WW w_0 q]] with ([|w_0|]*wB+[|q|]);rewrite spec_w_0;rewrite
   Z.mul_0_l;rewrite Z.add_0_l.
   replace [[ww_add_mul_div (ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c w_opp w_sub w_sub_carry
       _ww_zdigits (w_0W (w_head0 bh))) W0 r]] with ([[r]]/2^[|w_head0 bh|]).
   assert (0 < 2^[|w_head0 bh|]). apply Z.pow_pos_nonneg;zarith.
   split.
   rewrite <- (Z_div_mult [[WW ah al]] (2^[|w_head0 bh|]));zarith.
   rewrite H1;rewrite Z.mul_assoc;apply Z_div_plus_l;trivial.
   split;[apply Zdiv_le_lower_bound| apply Zdiv_lt_upper_bound];zarith.
   rewrite spec_ww_add_mul_div.
   rewrite spec_ww_sub; auto with zarith.
   rewrite spec_ww_digits_.
   change (Zpos (xO (w_digits))) with (2*Zpos (w_digits));zarith.
   simpl ww_to_Z;rewrite Z.mul_0_l;rewrite Z.add_0_l.
   rewrite spec_w_0W.
   rewrite (fun x y => Zmod_small (x-y)); auto with zarith.
   ring_simplify (2 * Zpos w_digits - (2 * Zpos w_digits - [|w_head0 bh|])).
   rewrite Zmod_small;zarith.
   split;[apply Zdiv_le_lower_bound| apply Zdiv_lt_upper_bound];zarith.
   Spec_ww_to_Z r.
   apply Z.lt_le_trans with wwB;zarith.
   rewrite <- (Z.mul_1_r wwB);apply Z.mul_le_mono_nonneg;zarith.
   split; auto with zarith.
   apply Z.le_lt_trans with (2 * Zpos w_digits); auto with zarith.
   unfold base, ww_digits; rewrite (Pos2Z.inj_xO w_digits).
   apply Zpower2_lt_lin; auto with zarith.
   rewrite spec_ww_sub; auto with zarith.
   rewrite spec_ww_digits_; rewrite spec_w_0W.
   rewrite Zmod_small;zarith.
   rewrite Pos2Z.inj_xO; split; auto with zarith.
   apply Z.le_lt_trans with (2 * Zpos w_digits); auto with zarith.
   unfold base, ww_digits; rewrite (Pos2Z.inj_xO w_digits).
   apply Zpower2_lt_lin; auto with zarith.
   Qed.

  Lemma spec_ww_div_gt : forall a b, [[a]] > [[b]] -> 0 < [[b]] ->
      let (q,r) := ww_div_gt a b in
      [[a]] = [[q]] * [[b]] + [[r]] /\
      0 <= [[r]] < [[b]].
  Proof.
   intros a b Hgt Hpos;unfold ww_div_gt.
   change (let (q,r) :=   match a, b with
  | W0, _ => (W0,W0)
  | _, W0 => (W0,W0)
  | WW ah al, WW bh bl =>
    if w_eq0 ah then
     let (q,r) := w_div_gt al bl in
     (WW w_0 q, w_0W r)
    else
     match w_compare w_0 bh with
     | Eq =>
       let(q,r):=
        double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21
                  w_compare w_sub 1 a bl in
       (q, w_0W r)
     | Lt => ww_div_gt_aux ah al bh bl
     | Gt => (W0,W0) (* cas absurde *)
     end
  end in [[a]] = [[q]] * [[b]] + [[r]] /\ 0 <= [[r]] < [[b]]).
   destruct a as [ |ah al]. simpl in Hgt;omega.
   destruct b as [ |bh bl]. simpl in Hpos;omega.
   Spec_w_to_Z ah; Spec_w_to_Z al; Spec_w_to_Z bh; Spec_w_to_Z bl.
   assert (H:=@spec_eq0 ah);destruct (w_eq0 ah).
   simpl ww_to_Z;rewrite H;trivial. simpl in Hgt;rewrite H in Hgt;trivial.
   assert ([|bh|] <= 0).
   apply beta_lex with (d:=[|al|])(b:=[|bl|]) (beta := wB);zarith.
   assert ([|bh|] = 0);zarith. rewrite H1 in Hgt;rewrite H1;simpl in Hgt.
   simpl. simpl in Hpos;rewrite H1 in Hpos;simpl in Hpos.
   assert (H2:=spec_div_gt Hgt Hpos);destruct (w_div_gt al bl).
   repeat rewrite spec_w_0W;simpl;rewrite spec_w_0;simpl;trivial.
   clear H.
   rewrite spec_compare; case Z.compare_spec; intros Hcmp.
   rewrite spec_w_0 in Hcmp. change [[WW bh bl]] with ([|bh|]*wB+[|bl|]).
   rewrite <- Hcmp;rewrite Z.mul_0_l;rewrite Z.add_0_l.
   simpl in Hpos;rewrite <- Hcmp in Hpos;simpl in Hpos.
   assert (H2:= @spec_double_divn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div
    w_div21 w_compare w_sub w_to_Z spec_to_Z spec_w_zdigits spec_w_0 spec_w_WW spec_head0
    spec_add_mul_div spec_div21 spec_compare spec_sub 1 (WW ah al) bl Hpos).
   destruct (double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21
              w_compare w_sub 1
             (WW ah al) bl).
   rewrite spec_w_0W;unfold ww_to_Z;trivial.
   apply spec_ww_div_gt_aux;trivial. rewrite spec_w_0 in Hcmp;trivial.
   rewrite spec_w_0 in Hcmp;exfalso;omega.
  Qed.

  Lemma spec_ww_mod_gt_aux_eq : forall ah al bh bl,
   ww_mod_gt_aux ah al bh bl = snd (ww_div_gt_aux ah al bh bl).
  Proof.
   intros ah al bh bl. unfold ww_mod_gt_aux, ww_div_gt_aux.
   case w_compare; auto.
   case w_div32; auto.
  Qed.

  Lemma spec_ww_mod_gt_aux : forall ah al bh bl,
   [[WW ah al]] > [[WW bh bl]] ->
    0 < [|bh|] ->
    [[ww_mod_gt_aux ah al bh bl]] = [[WW ah al]] mod [[WW bh bl]].
  Proof.
   intros. rewrite spec_ww_mod_gt_aux_eq;trivial.
   assert (H3 := spec_ww_div_gt_aux ah al bl H H0).
   destruct (ww_div_gt_aux ah al bh bl) as (q,r);simpl. simpl in H,H3.
   destruct H3;apply Zmod_unique with [[q]];zarith.
   rewrite H1;ring.
  Qed.

  Lemma spec_w_mod_gt_eq : forall a b, [|a|] > [|b|] -> 0 <[|b|] ->
    [|w_mod_gt a b|] = [|snd (w_div_gt a b)|].
  Proof.
   intros a b Hgt Hpos.
   rewrite spec_mod_gt;trivial.
   assert (H:=spec_div_gt Hgt Hpos).
   destruct (w_div_gt a b) as (q,r);simpl.
   rewrite Z.mul_comm in H;destruct H.
   symmetry;apply Zmod_unique with [|q|];trivial.
  Qed.

  Lemma spec_ww_mod_gt_eq : forall a b, [[a]] > [[b]] -> 0 < [[b]] ->
      [[ww_mod_gt a b]] = [[snd (ww_div_gt a b)]].
  Proof.
   intros a b Hgt Hpos.
   change (ww_mod_gt a b) with
   (match a, b with
  | W0, _ => W0
  | _, W0 => W0
  | WW ah al, WW bh bl =>
    if w_eq0 ah then w_0W (w_mod_gt al bl)
    else
     match w_compare w_0 bh with
     | Eq =>
       w_0W (double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21
             w_compare w_sub 1 a bl)
     | Lt => ww_mod_gt_aux ah al bh bl
     | Gt => W0 (* cas absurde *)
     end end).
   change (ww_div_gt a b) with
   (match a, b with
  | W0, _ => (W0,W0)
  | _, W0 => (W0,W0)
  | WW ah al, WW bh bl =>
    if w_eq0 ah then
     let (q,r) := w_div_gt al bl in
     (WW w_0 q, w_0W r)
    else
     match w_compare w_0 bh with
     | Eq =>
       let(q,r):=
        double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21
                  w_compare w_sub 1 a bl in
       (q, w_0W r)
     | Lt => ww_div_gt_aux ah al bh bl
     | Gt => (W0,W0) (* cas absurde *)
     end
  end).
   destruct a as [ |ah al];trivial.
   destruct b as [ |bh bl];trivial.
   Spec_w_to_Z ah; Spec_w_to_Z al; Spec_w_to_Z bh; Spec_w_to_Z bl.
   assert (H:=@spec_eq0 ah);destruct (w_eq0 ah).
   simpl in Hgt;rewrite H in Hgt;trivial.
   assert ([|bh|] <= 0).
   apply beta_lex with (d:=[|al|])(b:=[|bl|]) (beta := wB);zarith.
   assert ([|bh|] = 0);zarith. rewrite H1 in Hgt;simpl in Hgt.
   simpl in Hpos;rewrite H1 in Hpos;simpl in Hpos.
   rewrite spec_w_0W;rewrite spec_w_mod_gt_eq;trivial.
   destruct (w_div_gt al bl);simpl;rewrite spec_w_0W;trivial.
   clear H.
   rewrite spec_compare; case Z.compare_spec; intros H2.
   rewrite (@spec_double_modn1_aux w w_zdigits w_0 w_WW w_head0 w_add_mul_div
            w_div21 w_compare w_sub w_to_Z spec_w_0 spec_compare 1 (WW ah al) bl).
   destruct (double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub 1
             (WW ah al) bl);simpl;trivial.
   rewrite spec_ww_mod_gt_aux_eq;trivial;symmetry;trivial.
   trivial.
  Qed.

  Lemma spec_ww_mod_gt : forall a b, [[a]] > [[b]] -> 0 < [[b]] ->
      [[ww_mod_gt a b]] = [[a]] mod [[b]].
  Proof.
   intros a b Hgt Hpos.
   assert (H:= spec_ww_div_gt a b Hgt Hpos).
   rewrite (spec_ww_mod_gt_eq a b Hgt Hpos).
   destruct (ww_div_gt a b)as(q,r);destruct H.
   apply Zmod_unique with[[q]];simpl;trivial.
   rewrite Z.mul_comm;trivial.
  Qed.

  Lemma Zis_gcd_mod : forall a b d,
   0 < b -> Zis_gcd b (a mod b) d -> Zis_gcd a b d.
  Proof.
   intros a b d H H1; apply Zis_gcd_for_euclid with (a/b).
   pattern a at 1;rewrite (Z_div_mod_eq a b).
   ring_simplify (b * (a / b) + a mod b - a / b * b);trivial. zarith.
  Qed.

  Lemma spec_ww_gcd_gt_aux_body :
   forall ah al bh bl n cont,
    [[WW bh bl]] <= 2^n ->
    [[WW ah al]] > [[WW bh bl]] ->
    (forall xh xl yh yl,
     [[WW xh xl]] > [[WW yh yl]] -> [[WW yh yl]] <= 2^(n-1) ->
     Zis_gcd [[WW xh xl]] [[WW yh yl]] [[cont xh xl yh yl]]) ->
    Zis_gcd [[WW ah al]] [[WW bh bl]] [[ww_gcd_gt_body cont ah al bh bl]].
  Proof.
   intros ah al bh bl n cont Hlog Hgt Hcont.
   change (ww_gcd_gt_body cont ah al bh bl) with (match w_compare w_0 bh with
    | Eq =>
      match w_compare w_0 bl with
      | Eq => WW ah al (* normalement n'arrive pas si forme normale *)
      | Lt =>
	let m := double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21
                   w_compare w_sub 1 (WW ah al) bl in
        WW w_0 (w_gcd_gt bl m)
      | Gt => W0 (* absurde *)
      end
    | Lt =>
      let m := ww_mod_gt_aux ah al bh bl in
      match m with
      | W0 => WW bh bl
      | WW mh ml =>
        match w_compare w_0 mh with
        | Eq =>
          match w_compare w_0 ml with
          | Eq => WW bh bl
          | _  =>
            let r := double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21
                      w_compare w_sub 1 (WW bh bl) ml in
            WW w_0 (w_gcd_gt ml r)
          end
        | Lt =>
          let r := ww_mod_gt_aux bh bl mh ml in
          match r with
          | W0 => m
          | WW rh rl => cont mh ml rh rl
          end
        | Gt => W0 (* absurde *)
        end
      end
    | Gt => W0 (* absurde *)
    end).
   rewrite spec_compare, spec_w_0.
   case Z.compare_spec; intros Hbh.
   simpl ww_to_Z in *. rewrite <- Hbh.
   rewrite Z.mul_0_l;rewrite Z.add_0_l.
   rewrite spec_compare, spec_w_0.
   case Z.compare_spec; intros Hbl.
   rewrite <- Hbl;apply Zis_gcd_0.
   simpl;rewrite spec_w_0;rewrite Z.mul_0_l;rewrite Z.add_0_l.
   apply Zis_gcd_mod;zarith.
   change ([|ah|] * wB + [|al|]) with (double_to_Z w_digits w_to_Z 1 (WW ah al)).
   rewrite <- (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div
    w_div21 w_compare w_sub w_to_Z spec_to_Z spec_w_zdigits spec_w_0 spec_w_WW spec_head0 spec_add_mul_div
    spec_div21 spec_compare spec_sub 1 (WW ah al) bl Hbl).
   apply spec_gcd_gt.
   rewrite  (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW); trivial.
   apply Z.lt_gt;match goal with | |- ?x mod ?y < ?y =>
    destruct (Z_mod_lt x y);zarith end.
   Spec_w_to_Z bl;exfalso;omega.
   assert (H:= spec_ww_mod_gt_aux _ _ _ Hgt Hbh).
   assert (H2 : 0 < [[WW bh bl]]).
   simpl;Spec_w_to_Z bl. apply Z.lt_le_trans with ([|bh|]*wB);zarith.
   apply Z.mul_pos_pos;zarith.
   apply Zis_gcd_mod;trivial. rewrite <- H.
   simpl in *;destruct (ww_mod_gt_aux ah al bh bl) as [ |mh ml].
   simpl;apply Zis_gcd_0;zarith.
   rewrite spec_compare, spec_w_0; case Z.compare_spec; intros Hmh.
   simpl;rewrite <- Hmh;simpl.
   rewrite spec_compare, spec_w_0; case Z.compare_spec; intros Hml.
   rewrite <- Hml;simpl;apply Zis_gcd_0.
   simpl; rewrite spec_w_0; simpl.
   apply Zis_gcd_mod;zarith.
   change ([|bh|] * wB + [|bl|]) with (double_to_Z w_digits w_to_Z 1 (WW bh bl)).
   rewrite <- (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div
   w_div21 w_compare w_sub w_to_Z spec_to_Z spec_w_zdigits spec_w_0 spec_w_WW spec_head0 spec_add_mul_div
   spec_div21 spec_compare spec_sub 1 (WW bh bl) ml Hml).
   apply spec_gcd_gt.
   rewrite  (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW); trivial.
   apply Z.lt_gt;match goal with | |- ?x mod ?y < ?y =>
   destruct (Z_mod_lt x y);zarith end.
   Spec_w_to_Z ml;exfalso;omega.
   assert ([[WW bh bl]] > [[WW mh ml]]).
   rewrite H;simpl; apply Z.lt_gt;match goal with | |- ?x mod ?y < ?y =>
   destruct (Z_mod_lt x y);zarith end.
   assert (H1:= spec_ww_mod_gt_aux _ _ _ H0 Hmh).
   assert (H3 : 0 < [[WW mh ml]]).
   simpl;Spec_w_to_Z ml. apply Z.lt_le_trans with ([|mh|]*wB);zarith.
   apply Z.mul_pos_pos;zarith.
   apply Zis_gcd_mod;zarith. simpl in *;rewrite <- H1.
   destruct (ww_mod_gt_aux bh bl mh ml) as [ |rh rl]. simpl; apply Zis_gcd_0.
   simpl;apply Hcont. simpl in H1;rewrite H1.
   apply Z.lt_gt;match goal with | |- ?x mod ?y < ?y =>
   destruct (Z_mod_lt x y);zarith end.
   apply Z.le_trans with (2^n/2).
   apply Zdiv_le_lower_bound;zarith.
   apply Z.le_trans with ([|bh|] * wB + [|bl|]);zarith.
   assert (H3' := Z_div_mod_eq [[WW bh bl]] [[WW mh ml]] (Z.lt_gt _ _ H3)).
   assert (H4 : 0 <= [[WW bh bl]]/[[WW mh ml]]).
   apply Z.ge_le;apply Z_div_ge0;zarith. simpl in *;rewrite H1.
   pattern ([|bh|] * wB + [|bl|]) at 2;rewrite H3'.
   Z.le_elim H4.
   assert (H6' : [[WW bh bl]] mod [[WW mh ml]] =
                  [[WW bh bl]] - [[WW mh ml]] * ([[WW bh bl]]/[[WW mh ml]])).
   simpl;pattern ([|bh|] * wB + [|bl|]) at 2;rewrite H3';ring. simpl in H6'.
   assert ([[WW mh ml]] <= [[WW mh ml]] * ([[WW bh bl]]/[[WW mh ml]])).
   simpl;pattern ([|mh|]*wB+[|ml|]) at 1;rewrite <- Z.mul_1_r;zarith.
   simpl in *;assert (H8 := Z_mod_lt [[WW bh bl]] [[WW mh ml]]);simpl in H8;
    zarith.
   assert (H8 := Z_mod_lt [[WW bh bl]] [[WW mh ml]]);simpl in *;zarith.
   rewrite <- H4 in H3';rewrite Z.mul_0_r in H3';simpl in H3';zarith.
   pattern n at 1;replace n with (n-1+1);try ring.
   rewrite Zpower_exp;zarith. change (2^1) with 2.
   rewrite Z_div_mult;zarith.
   assert (2^1 <= 2^n). change (2^1) with 2;zarith.
   assert (H7 := @Zpower_le_monotone_inv 2 1 n);zarith.
   Spec_w_to_Z mh;exfalso;zarith.
   Spec_w_to_Z bh;exfalso;zarith.
  Qed.

  Lemma spec_ww_gcd_gt_aux :
   forall p cont n,
   (forall xh xl yh yl,
     [[WW xh xl]] > [[WW yh yl]] ->
     [[WW yh yl]] <= 2^n ->
      Zis_gcd [[WW xh xl]] [[WW yh yl]] [[cont xh xl yh yl]]) ->
   forall ah al bh bl , [[WW ah al]] > [[WW bh bl]] ->
     [[WW bh bl]] <= 2^(Zpos p + n) ->
     Zis_gcd [[WW ah al]] [[WW bh bl]]
        [[ww_gcd_gt_aux p cont ah al bh bl]].
  Proof.
   induction p;intros cont n Hcont ah al bh bl Hgt Hs;simpl ww_gcd_gt_aux.
   assert (0 < Zpos p). unfold Z.lt;reflexivity.
   apply spec_ww_gcd_gt_aux_body with (n := Zpos (xI p) + n);
   trivial;rewrite Pos2Z.inj_xI.
   intros. apply IHp with (n := Zpos p + n);zarith.
   intros. apply IHp with (n := n );zarith.
   apply Z.le_trans with (2 ^ (2* Zpos p + 1+ n -1));zarith.
   apply Z.pow_le_mono_r;zarith.
   assert (0 < Zpos p). unfold Z.lt;reflexivity.
   apply spec_ww_gcd_gt_aux_body with (n := Zpos (xO p) + n );trivial.
   rewrite (Pos2Z.inj_xO p).
   intros. apply IHp with (n := Zpos p + n - 1);zarith.
   intros. apply IHp with (n := n -1 );zarith.
   intros;apply Hcont;zarith.
   apply Z.le_trans with (2^(n-1));zarith.
   apply Z.pow_le_mono_r;zarith.
   apply Z.le_trans with (2 ^ (Zpos p + n -1));zarith.
   apply Z.pow_le_mono_r;zarith.
   apply Z.le_trans with (2 ^ (2*Zpos p + n -1));zarith.
   apply Z.pow_le_mono_r;zarith.
   apply spec_ww_gcd_gt_aux_body with (n := n+1);trivial.
   rewrite Z.add_comm;trivial.
   ring_simplify (n + 1 - 1);trivial.
  Qed.

End DoubleDivGt.

Section DoubleDiv.

 Variable w : Type.
 Variable w_digits : positive.
 Variable ww_1 : zn2z w.
 Variable ww_compare : zn2z w -> zn2z w -> comparison.

 Variable ww_div_gt : zn2z w -> zn2z w -> zn2z w * zn2z w.
 Variable ww_mod_gt : zn2z w -> zn2z w -> zn2z w.

 Definition ww_div a b :=
  match ww_compare a b with
  | Gt => ww_div_gt a b
  | Eq => (ww_1, W0)
  | Lt => (W0, a)
  end.

 Definition ww_mod a b :=
  match ww_compare a b with
  | Gt => ww_mod_gt a b
  | Eq => W0
  | Lt => a
  end.

  Variable w_to_Z : w -> Z.
  Notation wB  := (base w_digits).
  Notation wwB := (base (ww_digits w_digits)).
  Notation "[| x |]" := (w_to_Z x)  (at level 0, x at level 99).
  Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99).
  Variable spec_to_Z  : forall x, 0 <= [|x|] < wB.
  Variable spec_ww_1 : [[ww_1]] = 1.
  Variable spec_ww_compare :  forall x y,
    ww_compare x y = Z.compare [[x]] [[y]].
  Variable spec_ww_div_gt : forall a b, [[a]] > [[b]] -> 0 < [[b]] ->
      let (q,r) := ww_div_gt a b in
      [[a]] = [[q]] * [[b]] + [[r]] /\
      0 <= [[r]] < [[b]].
  Variable spec_ww_mod_gt : forall a b, [[a]] > [[b]] -> 0 < [[b]] ->
      [[ww_mod_gt a b]] = [[a]] mod [[b]].

  Ltac Spec_w_to_Z x :=
   let H:= fresh "HH" in
   assert (H:= spec_to_Z x).

  Ltac Spec_ww_to_Z x :=
   let H:= fresh "HH" in
   assert (H:= spec_ww_to_Z w_digits w_to_Z spec_to_Z x).

  Lemma spec_ww_div : forall a b, 0 < [[b]] ->
      let (q,r) := ww_div a b in
      [[a]] = [[q]] * [[b]] + [[r]] /\
      0 <= [[r]] < [[b]].
  Proof.
   intros a b Hpos;unfold ww_div.
   rewrite spec_ww_compare; case Z.compare_spec; intros.
   simpl;rewrite spec_ww_1;split;zarith.
   simpl;split;[ring|Spec_ww_to_Z a;zarith].
   apply spec_ww_div_gt;auto with zarith.
  Qed.

  Lemma  spec_ww_mod :  forall a b, 0 < [[b]] ->
      [[ww_mod a b]] = [[a]] mod [[b]].
  Proof.
   intros a b Hpos;unfold ww_mod.
   rewrite spec_ww_compare; case Z.compare_spec; intros.
   simpl;apply Zmod_unique with 1;try rewrite H;zarith.
   Spec_ww_to_Z a;symmetry;apply Zmod_small;zarith.
   apply spec_ww_mod_gt;auto with zarith.
  Qed.


 Variable w_0 : w.
 Variable w_1 : w.
 Variable w_compare : w -> w -> comparison.
 Variable w_eq0 : w -> bool.
 Variable w_gcd_gt : w -> w -> w.
 Variable _ww_digits : positive.
 Variable spec_ww_digits_ : _ww_digits = xO w_digits.
 Variable ww_gcd_gt_fix :
   positive -> (w -> w -> w -> w -> zn2z w) ->
             w -> w -> w -> w -> zn2z w.

  Variable spec_w_0   : [|w_0|] = 0.
  Variable spec_w_1   : [|w_1|] = 1.
  Variable spec_compare :
    forall x y, w_compare x y = Z.compare [|x|] [|y|].
  Variable spec_eq0 : forall x, w_eq0 x = true -> [|x|] = 0.
  Variable spec_gcd_gt : forall a b, [|a|] > [|b|] ->
      Zis_gcd [|a|] [|b|] [|w_gcd_gt a b|].
  Variable spec_gcd_gt_fix :
   forall p cont n,
   (forall xh xl yh yl,
     [[WW xh xl]] > [[WW yh yl]] ->
     [[WW yh yl]] <= 2^n ->
      Zis_gcd [[WW xh xl]] [[WW yh yl]] [[cont xh xl yh yl]]) ->
   forall ah al bh bl , [[WW ah al]] > [[WW bh bl]] ->
     [[WW bh bl]] <= 2^(Zpos p + n) ->
     Zis_gcd [[WW ah al]] [[WW bh bl]]
        [[ww_gcd_gt_fix p cont ah al bh bl]].

 Definition gcd_cont (xh xl yh yl:w) :=
  match w_compare w_1 yl with
  | Eq => ww_1
  | _ => WW xh xl
  end.

  Lemma spec_gcd_cont : forall xh xl yh yl,
     [[WW xh xl]] > [[WW yh yl]] ->
     [[WW yh yl]] <= 1 ->
      Zis_gcd [[WW xh xl]] [[WW yh yl]] [[gcd_cont xh xl yh yl]].
  Proof.
   intros xh xl yh yl Hgt' Hle. simpl in Hle.
   assert ([|yh|] = 0).
    change 1 with (0*wB+1) in Hle.
    assert (0 <= 1 < wB). split;zarith. apply wB_pos.
    assert (H1:= beta_lex _ _ _ _ _ Hle (spec_to_Z yl) H).
    Spec_w_to_Z yh;zarith.
   unfold gcd_cont; rewrite spec_compare, spec_w_1.
   case Z.compare_spec; intros Hcmpy.
   simpl;rewrite H;simpl;
   rewrite spec_ww_1;rewrite <- Hcmpy;apply Zis_gcd_mod;zarith.
   rewrite <- (Zmod_unique ([|xh|]*wB+[|xl|]) 1 ([|xh|]*wB+[|xl|]) 0);zarith.
   rewrite H in Hle; exfalso;zarith.
   assert (H0 : [|yl|] = 0) by (Spec_w_to_Z yl;zarith).
   simpl. rewrite H0, H;simpl;apply Zis_gcd_0;trivial.
  Qed.


  Variable cont : w -> w -> w -> w -> zn2z w.
  Variable spec_cont : forall xh xl yh yl,
     [[WW xh xl]] > [[WW yh yl]] ->
     [[WW yh yl]] <= 1 ->
      Zis_gcd [[WW xh xl]] [[WW yh yl]] [[cont xh xl yh yl]].

  Definition ww_gcd_gt a b :=
   match a, b with
   | W0, _ => b
   | _, W0 => a
   | WW ah al, WW bh bl =>
     if w_eq0 ah then (WW w_0 (w_gcd_gt al bl))
     else ww_gcd_gt_fix _ww_digits cont ah al bh bl
   end.

  Definition ww_gcd a b :=
   Eval lazy beta delta [ww_gcd_gt] in
   match ww_compare a b with
   | Gt => ww_gcd_gt a b
   | Eq => a
   | Lt => ww_gcd_gt b a
   end.

  Lemma spec_ww_gcd_gt : forall a b, [[a]] > [[b]] ->
      Zis_gcd [[a]] [[b]] [[ww_gcd_gt a b]].
  Proof.
   intros a b Hgt;unfold ww_gcd_gt.
   destruct a as [ |ah al]. simpl;apply Zis_gcd_sym;apply Zis_gcd_0.
   destruct b as [ |bh bl]. simpl;apply Zis_gcd_0.
   simpl in Hgt. generalize (@spec_eq0 ah);destruct (w_eq0 ah);intros.
   simpl;rewrite H in Hgt;trivial;rewrite H;trivial;rewrite spec_w_0;simpl.
   assert ([|bh|] <= 0).
   apply beta_lex with (d:=[|al|])(b:=[|bl|]) (beta := wB);zarith.
   Spec_w_to_Z bh;assert ([|bh|] = 0);zarith. rewrite H1 in Hgt;simpl in Hgt.
   rewrite H1;simpl;auto. clear H.
   apply spec_gcd_gt_fix with (n:= 0);trivial.
   rewrite Z.add_0_r;rewrite spec_ww_digits_.
   change (2 ^ Zpos (xO w_digits)) with wwB. Spec_ww_to_Z (WW bh bl);zarith.
  Qed.

  Lemma spec_ww_gcd : forall a b, Zis_gcd [[a]] [[b]] [[ww_gcd a b]].
  Proof.
   intros a b.
   change (ww_gcd a b) with
    (match ww_compare a b with
     | Gt => ww_gcd_gt a b
     | Eq => a
     | Lt => ww_gcd_gt b a
     end).
   rewrite spec_ww_compare; case Z.compare_spec; intros Hcmp.
   Spec_ww_to_Z b;rewrite Hcmp.
   apply Zis_gcd_for_euclid with 1;zarith.
   ring_simplify ([[b]] - 1 * [[b]]). apply Zis_gcd_0;zarith.
   apply Zis_gcd_sym;apply spec_ww_gcd_gt;zarith.
   apply spec_ww_gcd_gt;zarith.
  Qed.

End DoubleDiv.