Index: /src/ASM/Assembly.ma
===================================================================
--- /src/ASM/Assembly.ma	(revision 2190)
+++ /src/ASM/Assembly.ma	(revision 2191)
@@ -1042,6 +1042,16 @@
       cases (IH ?) -IH
       [2: %1 cases OR_lt_eq
-        [ normalize nodelta >nat_of_bitvector_add
-          [2: cases daemon (*CSC: should be true*)]
+        [ normalize nodelta #LT lapply LT >nat_of_bitvector_add
+          [2: >nat_of_bitvector_bitvector_of_nat_inverse [2: //]
+            cases (le_to_or_lt_eq … (? : nat_of_bitvector … ppc < 2^16))
+            [ #X <plus_n_Sm <plus_n_O @X
+            | #abs @⊥
+              cut (∀n,m,r. m + r = 2^n → add n (bitvector_of_nat n m) (bitvector_of_nat n r) = zero n)
+              [ cases daemon (* CSC: put in library *) ] #add_overflow
+              <(bitvector_of_nat_inverse_nat_of_bitvector … ppc) in LT;
+              >add_overflow [2: <plus_n_Sm <plus_n_O assumption ]
+              #abs' @(absurd … abs') normalize in ⊢ (? (??%));
+              @not_le_Sn_O
+            | @(lt_to_le_to_lt … ppc_ok) assumption ]]
           >nat_of_bitvector_bitvector_of_nat_inverse [2: // ]
           <plus_n_Sm <plus_n_O #X lapply (le_S_S_to_le … X) -X #X