Commit 265b01b0 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

Change notation and proof of multiplication in GF

ToFF changed to  ZofList or Z.lst or Z16.lst depending on the context
:P (as for the finite field) changed to :GF
parent 6378c44b
Require Export SumList.
Require Export ToFF.
Require Export ZofList.
Import ListNotations.
Open Scope Z.
Lemma ZsumListToFF : forall n a b o, a b = o -> ToFF n a + ToFF n b = ToFF n o.
Section Integer.
Variable n:Z.
Hypothesis Hn: n > 0.
Notation "ℤ.lst A" := (ZofList n A) (at level 65, right associativity).
Lemma ZsumList_correct_impl : forall a b o, a b = o -> (.lst a) + (.lst b) = .lst o.
Proof.
intro n ; induction a , b.
induction a , b.
- intros o HSum ; go.
- intros o HSum ; go.
- intros o HSum ; go.
......@@ -17,8 +24,7 @@ intro n ; induction a , b.
apply headSame in Hh.
apply tailSame in HSum.
apply IHa in HSum.
unfold ToFF.
unfold ToFF.ToFF.
unfold ZofList.
rewrite <- Z.add_shuffle2.
rewrite Zred_factor4.
apply Zplus_eq_compat.
......@@ -28,9 +34,11 @@ intro n ; induction a , b.
apply HSum.
Qed.
Corollary ZsumListToFF2: forall n a b, ToFF n (a b) = ToFF n a + ToFF n b.
Corollary ZsumList_correct: forall a b, (.lst a b) = (.lst a) + (.lst b).
Proof.
intros n a b.
intros a b.
assert(exists o, o = a b) by (exists (a b) ; go) ; destruct H.
symmetry; subst x ; apply ZsumListToFF ; go.
symmetry; subst x ; apply ZsumList_correct_impl ; go.
Qed.
End Integer.
Require Export A.
Require Export ZofList.
Require Export Reduce.
Import ListNotations.
Require Import Coq.Init.Datatypes.
Section FiniteFied.
Section Integer.
Variable n:Z.
Hypothesis Hn: n > 0.
Notation "ℤ.lst A" := (ZofList n A) (at level 65, right associativity).
Definition getCarry (m:Z) : Z := Z.shiftr m n.
(* Compute (getCarry (Z.pow 2 18)). *)
......@@ -95,13 +96,13 @@ induction l as [|h q IHl]; intros [] a Hm; simpl ; flatten ; go.
Qed.
Lemma CarryPreserveConst : forall l a , a + ToFF n l = ToFF n (Carrying a l).
Lemma CarryPreserveConst : forall l a , a + (.lst l) = .lst Carrying a l.
Proof.
induction l as [| h q IHl].
intro a ; destruct a ; assert(Hn0: 2 ^ n * 0 = 0) by (symmetry ; apply Zmult_0_r_reverse) ; simpl ; try rewrite Hn0 ; go.
intro a ; unfold Carrying ; fold Carrying.
flatten ;
unfold ToFF ; fold ToFF ; rewrite <- IHl ;
unfold ZofList ; fold ZofList ; rewrite <- IHl ;
rewrite <- Zplus_assoc_reverse ;
rewrite <- Zred_factor4 ;
rewrite <- Zplus_assoc_reverse ;
......@@ -109,13 +110,13 @@ rewrite residuteCarry ;
reflexivity.
Qed.
Lemma CarrynPreserveConst : forall m l a , a + ToFF n l = ToFF n (Carrying_n m a l).
Lemma CarrynPreserveConst : forall m l a , a + (.lst l) = .lst Carrying_n m a l.
Proof.
assert(Hn0: 2 ^ n * 0 = 0) by (symmetry ; apply Zmult_0_r_reverse).
induction m ; intros l a.
- simpl ; flatten ; try rewrite <- ToFF_add ; go.
- simpl ; flatten ; try rewrite <- ZofList_add ; go.
- simpl ; flatten ; go ;
rewrite! ToFF_cons ;
rewrite! ZofList_cons ;
rewrite <- IHm ;
rewrite <- Zplus_assoc_reverse ;
rewrite <- Zred_factor4 ;
......@@ -123,21 +124,21 @@ induction m ; intros l a.
rewrite residuteCarry ; go.
Qed.
Corollary CarryPreserve : forall l, ToFF n l = ToFF n (Carrying 0 l).
Corollary CarryPreserve : forall l, .lst l = .lst Carrying 0 l.
Proof.
intros.
replace (ToFF n l) with (0 + ToFF n l) by go.
replace (.lst l) with (0 + .lst l) by go.
apply CarryPreserveConst.
Qed.
Corollary CarrynPreserve : forall m l, ToFF n l = ToFF n (Carrying_n m 0 l).
Corollary CarrynPreserve : forall m l, .lst l = .lst Carrying_n m 0 l.
Proof.
intros.
replace (ToFF n l) with (0 + ToFF n l) by go.
replace (.lst l) with (0 + .lst l) by go.
apply CarrynPreserveConst.
Qed.
End FiniteFied.
End Integer.
Definition backCarry (l:list Z) : (list Z) :=
match l with
......@@ -146,14 +147,14 @@ Definition backCarry (l:list Z) : (list Z) :=
(h + 38 * getCarry 16 v) :: slice 14 q ++ [getResidute 16 v]
end.
Lemma backCarry_ToFF_25519 : forall l, (length l <= 16)%nat -> ToFF 16 l :𝓟 = (ToFF 16 (backCarry l) :𝓟).
Lemma backCarry_ToFF_25519 : forall l, (length l <= 16)%nat -> (16.lst l) :𝓖𝓕 = ((16.lst backCarry l) :𝓖𝓕).
Proof.
destruct l as [| h l]; intro Hlength.
- go.
- unfold backCarry.
rewrite ToFF_cons.
rewrite ToFF_cons.
rewrite ToFF_app ; try omega.
rewrite ZofList_cons.
rewrite ZofList_cons.
rewrite ZofList_app ; try omega.
apply le_lt_eq_dec in Hlength.
destruct Hlength.
+ rename l0 into H.
......@@ -163,7 +164,7 @@ destruct l as [| h l]; intro Hlength.
replace (slice 14 l) with l.
rewrite getResidute_0.
rewrite getCarry_0.
replace (ToFF 16 [0]) with 0.
replace (16.lst [0]) with 0.
f_equal.
ring.
go.
......@@ -196,10 +197,10 @@ destruct l as [| h l]; intro Hlength.
replace (slice 14 [z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12; z13]) with
[z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12] by go.
replace ([z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12; z13]) with ([z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12] ++ [ z13]) by go.
rewrite ToFF_app ; try omega.
rewrite ZofList_app ; try omega.
replace (length [z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12]) with 14%nat by go.
replace (ToFF 16 [getResidute 16 z13]) with (getResidute 16 z13) by go.
replace (ToFF 16 [z13]) with z13 by go.
replace (16.lst [getResidute 16 z13]) with (getResidute 16 z13) by go.
replace (16.lst [z13]) with z13 by go.
rewrite <- Zred_factor4.
rewrite <- Zred_factor4.
rewrite Zplus_assoc_reverse.
......@@ -247,7 +248,7 @@ Qed.
Definition car25519 (l:list Z) : list Z := backCarry (Carrying_n 16 14 0 l).
Lemma car25519_ToFF_25519 : forall l, (length l = 16)%nat -> ToFF 16 l :𝓟 = (ToFF 16 (car25519 l) :𝓟).
Lemma car25519_ToFF_25519 : forall l, (length l = 16)%nat -> (16.lst l) :𝓖𝓕 = (16.lst car25519 l) :𝓖𝓕.
Proof.
intros l Hlength.
unfold car25519.
......
Require Export SumList.
Require Export ToFF.
Require Export ScalarMult.
Require Export A.
Import ListNotations.
......@@ -21,45 +19,61 @@ Definition M (a b:list Z) : list Z :=
let m2 := mult_2 m1 in
mult_3 m2.
Lemma MultToFF' : forall (n:Z) (a b c: list Z), mult_1 a b = c -> ToFF n a * ToFF n b = ToFF n c.
Section Integer.
Variable n:Z.
Hypothesis Hn: n > 0.
Notation "ℤ.lst A" := (ZofList n A) (at level 65, right associativity).
Lemma mult1_correct_impl : forall (a b c: list Z), mult_1 a b = c -> (.lst a) * (.lst b) = .lst c.
Proof.
intro n ; induction a, b ; intros c Hc.
induction a, b ; intros c Hc.
- simpl in *; go.
- simpl in *; go.
- simpl in Hc.
rewrite Z.mul_comm.
go.
- rewrite! ToFF_cons.
- rewrite! ZofList_cons.
unfold mult_1 in Hc; fold mult_1 in Hc.
rewrite <- Hc.
rewrite ToFF_cons.
rewrite ZsumListToFF2.
rewrite ZofList_cons.
rewrite ZsumList_correct.
rewrite <- (IHa (z :: b) (mult_1 a0 (z :: b))) by go.
rewrite ToFF_cons.
rewrite ZscalarMultToFF.
rewrite ZofList_cons.
rewrite ZscalarMult_correct.
ring.
Qed.
Lemma mult_2_ToFF : forall (n:Z) (l: list Z), ToFF n (mult_2 l) = ToFF n l + 38 * ToFF n (tail (16%nat) l).
Corollary mult1_correct : forall (a b: list Z), .lst mult_1 a b = (.lst a) * (.lst b).
Proof.
intros a b.
symmetry.
erewrite mult1_correct_impl ; go.
Qed.
Lemma mult_2_correct : forall (l: list Z), (.lst mult_2 l) = (.lst l) + 38 * .lst tail 16 l.
Proof.
intros n l.
intros l.
unfold mult_2.
rewrite ZsumListToFF2.
rewrite ZscalarMultToFF.
rewrite ZsumList_correct.
rewrite ZscalarMult_correct.
go.
Qed.
Lemma reduce_slice_ToFF:
End Integer.
Lemma reduce_slice_GF:
forall (l:list Z),
Z.of_nat (length l) < 32 ->
(ToFF 16 (mult_3 (mult_2 l)) :𝓟) = (ToFF 16 l :𝓟).
. length l < 32 ->
(16.lst mult_3 (mult_2 l)) :𝓖𝓕 = (16.lst l) :𝓖𝓕.
Proof.
intros l Hl.
unfold mult_3.
unfold mult_2.
rewrite ToFF_slice ; try omega.
rewrite ZsumListToFF2.
rewrite ZscalarMultToFF.
rewrite ZofList_slice ; try omega.
rewrite ZsumList_correct.
rewrite ZscalarMult_correct.
assert(Hlength: (length l <= 16 \/ length l > 16)%nat) by omega.
destruct Hlength.
{
......@@ -72,12 +86,12 @@ destruct Hlength.
rewrite ZsumList_nil_r.
rewrite Ht.
rewrite Hs.
rewrite ToFF_nil.
rewrite ZofList_nil.
f_equal.
ring.
}
{
assert(Hlength: length (slice 16 (ZsumList l (ZscalarMult 38 (tail 16 l)))) = 16%nat).
assert(Hlength: length (slice 16 (l 38 tail 16 l)) = 16%nat).
rewrite slice_length_min.
rewrite ZsumList_length_max.
rewrite ZscalarMult_length.
......@@ -93,8 +107,8 @@ destruct Hlength.
rewrite Htailtail; clear Htailtail.
rewrite ZscalarMultnil.
rewrite ZsumList_nil_r.
replace (16 * Z.of_nat 16) with 256 by go.
assert(Hnul: (38 * ToFF 16 (tail 16 l) - 2 ^ 256 * ToFF 16 (tail 16 l)) mod (2 ^ 255 - 19) = 0).
replace (16 * . 16) with 256 by go.
assert(Hnul: (38 * (16.lst tail 16 l) - 2 ^ 256 * (16.lst tail 16 l)) :𝓖𝓕 = 0).
rewrite <- Zmult_minus_distr_r.
rewrite Zmult_mod.
replace ((38 - 2 ^ 256) mod (2 ^ 255 - 19)) with 0; compute ; reflexivity.
......@@ -105,3 +119,77 @@ destruct Hlength.
reflexivity.
}
Qed.
Lemma Zsucc16 : Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ (Z.succ 0))))))))))))))) = 16.
Proof.
compute ; reflexivity.
Qed.
Corollary mult_GF: forall a b, . length a = 16 -> . length b = 16 -> (16.lst M a b) :𝓖𝓕 = (16.lst a) * (16.lst b) :𝓖𝓕.
Proof.
intros a b Hla Hlb.
unfold M.
rewrite reduce_slice_GF.
f_equal.
rewrite mult1_correct.
go.
rewrite <- Zlength_correct in *.
destruct a ; [inversion Hla|]. (* 0 *)
destruct a ; [inversion Hla|]. (* 1 *)
destruct a ; [inversion Hla|]. (* 2 *)
destruct a ; [inversion Hla|]. (* 3 *)
destruct a ; [inversion Hla|]. (* 4 *)
destruct a ; [inversion Hla|]. (* 5 *)
destruct a ; [inversion Hla|]. (* 6 *)
destruct a ; [inversion Hla|]. (* 7 *)
destruct a ; [inversion Hla|]. (* 8 *)
destruct a ; [inversion Hla|]. (* 9 *)
destruct a ; [inversion Hla|]. (* 10 *)
destruct a ; [inversion Hla|]. (* 11 *)
destruct a ; [inversion Hla|]. (* 12 *)
destruct a ; [inversion Hla|]. (* 13 *)
destruct a ; [inversion Hla|]. (* 14 *)
destruct a ; [inversion Hla|]. (* 15 *)
destruct a ; [inversion Hla|]. (* 16 *)
- destruct b ; [inversion Hlb|]. (* 0 *)
destruct b ; [inversion Hlb|]. (* 1 *)
destruct b ; [inversion Hlb|]. (* 2 *)
destruct b ; [inversion Hlb|]. (* 3 *)
destruct b ; [inversion Hlb|]. (* 4 *)
destruct b ; [inversion Hlb|]. (* 5 *)
destruct b ; [inversion Hlb|]. (* 6 *)
destruct b ; [inversion Hlb|]. (* 7 *)
destruct b ; [inversion Hlb|]. (* 8 *)
destruct b ; [inversion Hlb|]. (* 9 *)
destruct b ; [inversion Hlb|]. (* 10 *)
destruct b ; [inversion Hlb|]. (* 11 *)
destruct b ; [inversion Hlb|]. (* 12 *)
destruct b ; [inversion Hlb|]. (* 13 *)
destruct b ; [inversion Hlb|]. (* 14 *)
destruct b ; [inversion Hlb|]. (* 15 *)
destruct b. (* 16 *)
+ simpl.
rewrite! Zlength_cons.
rewrite Zlength_nil.
compute. (* LOL ! Thx God ! *)
reflexivity.
+ clear Hla. exfalso. (* lets get a bit of visibility *)
rewrite! Zlength_cons in Hlb.
rewrite <- Zsucc16 in Hlb ;
repeat (rewrite Z.succ_inj_wd in Hlb).
rewrite Zlength_correct in Hlb.
rewrite <- Nat2Z.inj_succ in Hlb.
rewrite <- Nat2Z.inj_0 in Hlb.
rewrite Nat2Z.inj_iff in Hlb.
inversion Hlb.
- clear Hlb. exfalso. (* lets get a bit of visibility *)
rewrite! Zlength_cons in Hla.
rewrite <- Zsucc16 in Hla ;
repeat (rewrite Z.succ_inj_wd in Hla).
rewrite Zlength_correct in Hla.
rewrite <- Nat2Z.inj_succ in Hla.
rewrite <- Nat2Z.inj_0 in Hla.
rewrite Nat2Z.inj_iff in Hla.
inversion Hla.
Qed.
......@@ -3,9 +3,9 @@ Require Export notations.
Open Scope Z.
Notation "A :𝓟" := (A mod (2^255 - 19)) (at level 80, right associativity).
(*Notation "A :𝓖𝓕" := (A mod (2^255 - 19)) (at level 80, right associativity).*)
Lemma t2256is38 : (2^256 :𝓟 ) = (38 :𝓟).
Lemma t2256is38 : (2^256 :𝓖𝓕 ) = (38 :𝓖𝓕).
Proof.
compute.
reflexivity.
......@@ -24,7 +24,7 @@ Definition reduce n :=
let c := n / 2^(256) in
n + 38 * c - 2^(256) * c.
Lemma reduceFF : forall m, (reduce m :𝓟) = (m :𝓟).
Lemma reduceFF : forall m, (reduce m :𝓖𝓕) = (m :𝓖𝓕).
Proof.
intro m.
unfold reduce.
......
Require Export ToFF.
Require Export ZofList.
Import ListNotations.
Require Import Tools.
......@@ -11,16 +11,6 @@ end.
Notation "A ∘ B" := (ZscalarMult A B) (at level 60, right associativity).
Lemma ZscalarMultToFF: forall n a b, ToFF n (a b) = a * ToFF n b.
Proof.
intros n a.
induction b ; go.
unfold ZscalarMult ; fold ZscalarMult.
rewrite! ToFF_cons.
rewrite IHb.
ring.
Qed.
Lemma ZscalarMultnil : forall n, n [] = [].
Proof.
go.
......@@ -41,4 +31,22 @@ Proof.
induction l ; intros [] m; go.
Qed.
Section Integer.
Variable n:Z.
Hypothesis Hn: n > 0.
Notation "ℤ.lst A" := (ZofList n A) (at level 65, right associativity).
Lemma ZscalarMult_correct: forall a b, .lst a b = a * .lst b.
Proof.
intros a ; induction b ; go.
unfold ZscalarMult ; fold ZscalarMult.
rewrite! ZofList_cons.
rewrite IHb.
ring.
Qed.
End Integer.
Close Scope Z.
......@@ -5,7 +5,7 @@ Open Scope Z.
Import ListNotations.
Section FiniteFied.
Section Integer.
Variable n:Z.
Hypothesis Hn: n > 0.
......@@ -33,17 +33,18 @@ change (2 ^ 64) with (2 ^ 63 * 2).
intros; omega.
Qed.
Fixpoint ToFFi (a: list Z) (i:Z) : Z := match a with
(*
Fixpoint ZofListi (a: list Z) (i:Z) : Z := match a with
| [] => 0
| h :: q => h * Z.pow 2 (n * i) + ToFFi q (Z.succ i)
| h :: q => h * Z.pow 2 (n * i) + ZofListi q (Z.succ i)
end.
*)
Fixpoint ToFF (a : list Z) : Z := match a with
Fixpoint ZofList (a : list Z) : Z := match a with
| [] => 0
| h :: q => h + Z.pow 2 n * ToFF q
| h :: q => h + Z.pow 2 n * ZofList q
end.
Notation "ℤ.lst A" := (ZofList A) (at level 65, right associativity).
Lemma pown: 2 ^ n > 1.
Proof.
......@@ -56,13 +57,13 @@ Proof.
assert(Hp:= pown).
omega.
Qed.
Lemma ToFF_eq : forall l i, i >= 0 -> ToFFi l i = 2^(n * i) * ToFF l.
(*
Lemma ZofList_eq : forall l i, i >= 0 -> ZofListi l i = 2^(n * i) * ZofList l.
Proof.
dependent induction l; go.
intros i Hi.
unfold ToFFi ; fold ToFFi.
unfold ToFF ; fold ToFF.
unfold ZofListi ; fold ZofListi.
unfold ZofList ; fold ZofList.
assert (H := Hi).
apply IHl in H.
rewrite <- Zred_factor4.
......@@ -81,53 +82,54 @@ apply Zmult_gt_0_le_0_compat ; omega.
Qed.
Corollary ToFF_eq_D : forall l, ToFFi l 0 = ToFF l.
ZofListllary ZofList_eq_D : forall l, ZofListi l 0 = ZofList l.
Proof.
intro l.
assert (2^(n * 0) = 1) by (rewrite <- Zmult_0_r_reverse ; go).
assert (ToFF l = 2^(n * 0) * ToFF l).
assert (ZofList l = 2^(n * 0) * ZofList l).
rewrite H.
rewrite Z.mul_comm ; go.
rewrite H0.
apply ToFF_eq.
apply ZofList_eq.
omega.
Qed.
*)
Lemma ToFF_nil : ToFF nil = 0.
Lemma ZofList_nil : .lst nil = 0.
Proof.
go.
Qed.
Lemma ToFF_cons : forall a b, ToFF (a :: b) = a + 2^n * ToFF b.
Lemma ZofList_cons : forall a b, .lst a :: b = a + 2^n * .lst b.
Proof.
intros a b ; go.
Qed.
Lemma ToFF_add : forall m a b, ToFF (m + a :: b) = m + ToFF (a :: b).
Lemma ZofList_add : forall m a b, .lst m + a :: b = m + .lst a :: b.
Proof.
intros m a b ; go.
Qed.
Lemma ToFF_app : forall a b, ToFF (a ++ b) = ToFF a + 2^(n * . (length a)) * ToFF b.
Lemma ZofList_app : forall a b, .lst a ++ b = (.lst a) + 2^(n * . (length a)) * .lst b.
Proof.
induction a as [| h a Hl].
- intro b.
rewrite ToFF_nil.
rewrite ZofList_nil.
assert ([] ++ b = b) by apply app_nill_l. rewrite H ; go ; clear H.
assert (. (length (nil:(list Z))) = 0) by go. rewrite H ; go ; clear H.
assert (. length (nil:(list Z)) = 0) by go. rewrite H ; go ; clear H.
rewrite <- Zmult_0_r_reverse.
rewrite Z.pow_0_r.
omega.
- intro b.
assert ((h::a) ++ b = h :: a ++ b) by apply consApp2 ; rewrite H ; clear H.
unfold ToFF; fold ToFF.
unfold ZofList; fold ZofList.
rewrite Hl.
rewrite Zplus_assoc_reverse.
f_equal.
rewrite <- Zred_factor4.
f_equal.
rewrite <- Zmult_assoc_reverse.
assert(. (length (h :: a)) = . (1 + length a)) by go ; rewrite H ; clear H.
assert(. length (h :: a) = . 1 + length a) by go ; rewrite H ; clear H.
rewrite Nat2Z.inj_add.
assert(. 1 = 1) by go ; rewrite H ; clear H.
rewrite <- Zred_factor4.
......@@ -138,58 +140,58 @@ rewrite Z.mul_comm.
apply Zmult_gt_0_le_0_compat ; omega.
Qed.
Lemma ToFF_app_null: forall l, ToFF l = ToFF (l ++ [0]).
Lemma ZofList_app_null: forall l, .lst l = .lst l ++ [0].
Proof.
intro l.
rewrite ToFF_app.
rewrite ZofList_app.
simpl ; ring.
Qed.
Theorem ToFF_transitive: forall (f g:list Z -> list Z) f' g' l l',
ToFF (g l) = g' (ToFF l) ->
ToFF (f l') = f' (ToFF l') ->
Theorem ZofList_transitive: forall (f g:list Z -> list Z) f' g' l l',
.lst g l = g' (.lst l) ->
.lst f l' = f' (.lst l') ->
g l = l' ->
ToFF (f (g l)) = f' (g' (ToFF l)).
.lst f (g l) = f' (g' (.lst l)).
Proof.
go.
Qed.
Lemma ToFF_tail : forall l (m:nat),
2^(n * . (length (slice m l))) * ToFF (tail m l) = ToFF l - ToFF (slice m l).
Lemma ZofList_tail : forall l (m:nat),
2^(n * . length (slice m l)) * (.lst tail m l) = (.lst l) - .lst slice m l.
Proof.
intros l; destruct l; intros m.
simpl.
rewrite slice_length_le ; go.
rewrite tail_length_le ; go.
assert(HS: 2^(n * . (length (slice m (z::l)))) * ToFF (tail m (z :: l)) = 2^(n * . (length (slice m (z::l)))) * ToFF (tail m (z :: l)) - ToFF (slice m (z :: l)) + ToFF (slice m (z :: l))) by omega.
assert(HS: 2^(n * . length (slice m (z::l))) * (.lst tail m (z :: l)) = 2^(n * . length (slice m (z::l))) * (.lst tail m (z :: l)) - (.lst slice m (z :: l)) + (.lst slice m (z :: l))) by omega.
rewrite HS ; clear HS.
rewrite <- Z.add_sub_swap.
f_equal.
rewrite Z.add_comm.
rewrite <- ToFF_app ; go.
rewrite <- ZofList_app ; go.
assert(HS: slice m (z :: l) ++ tail m (z :: l) = z :: l).
apply slice_tail_app.
rewrite HS ; clear HS.
go.