+ simplify in ⊢ (? ? ? %);
+ change in ⊢ (? ? % ?) with
+ (update
+ (update
+ (update
+ (update (update (mult_memory x y) 30 x) 31
+ (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
+ (byte_of_nat (nat_of_byte y-S n)))
+ (nat_of_byte
+ (update
+ (update
+ (update (update (mult_memory x y) 30 x) 31
+ (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
+ (byte_of_nat (nat_of_byte y-S n)) 15))
+ (byte_of_nat (nat_of_byte x*S n)) a);
+ normalize in ⊢ (? ? (? ? % ? ?) ?);
+ apply inj_update;
+ intro;
+ apply inj_update;
+ intro;
+ rewrite > not_eq_a_b_to_eq_update_a_b in ⊢ (? ? % ?); [2: apply H | ];
+ rewrite > not_eq_a_b_to_eq_update_a_b in ⊢ (? ? % ?);
+ [ reflexivity
+ | assumption
+ ]