[Algorytmy] Poprawność algorytmu na średnią harmoniczną

Witam. Mam za zadanie dowieść poprawność algorytmu obliczającego średnią harmoniczną N liczb. Wygląda to tak:

s:=a[1];
for i=2 to N do
   s:=i/((1/s)/(i-1)+1/a[i]);

Zmieniłem ten kod na pętlę while i wygląda on teraz tak:

s:=a[1];
i:=2;
while i=<N do
   begin
      s:=i/((1/s)/(i-1)+1/a[i]); 
      i:=i+1;
   end;

Warunek końcowy ma postać:

         n
{s=N / Σ 1/a[k]
      k=1

Ustaliłem, że niezmiennik pętli powinien wyglądać tak:

          
        i-1
P={s=N / Σ 1/a[k]
        k=1

I teraz mam problem, bo nie wychodzi mi przekształcenie (P^B) w taki sposób, żeby móc wykonać instrukcję podstawienia za s. Czy ktoś może mi pomóc w jakiś sposób?