proposition: Lemma safeAccE i a b : safeAcc i a b =1 safeAcc_scanl (Z_of_nat i) a b.
proof: Proof. move=> s; elim: s i a b => // h t IH i a b. rewrite /safeAcc_scanl /=. move: (IH i.+1 ((Z.of_nat i + h) :: a) ((Z.of_nat i - h) :: b))%Z. rewrite (_ : Z.of_nat i.+1 = (Z.of_nat i) + 1)%Z; last by rewrite -addn1 Nat2Z.inj_add. rewrite /safeAcc_scanl => /= <-. rewrite /safeAcc /= !andbA /zipWith /=. set A := uniq _. set B := uniq _. set sa := map _ _. set sb := map _ _. rewrite -![in LHS]andbA [in LHS]andbC. do 2 rewrite -![in RHS]andbA [in RHS]andbC. rewrite -!andbA; congr andb. rewrite -[in LHS]andbC -!andbA; congr andb. do 2 rewrite ![in RHS]andbA [in RHS]andbC. congr andb. rewrite [in LHS]andbCA -![in RHS]andbA; congr andb. have H : forall (op : Z -> Z -> Z) y s, all (fun x : Z => x \notin op (Z_of_nat i) h :: y) s = all (fun x : Z => x \notin y) s && (op (Z_of_nat i) h \notin s). move=> op y; elim => //= s1 s2 ih /=; rewrite ih !inE !negb_or. rewrite -andbA andbCA !andbA; congr (_ && _); rewrite -!andbA; congr(_ && _). by rewrite andbC eq_sym. by rewrite andbA andbCA -!andbA andbCA !andbA -H -andbA -H. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib