Rigorous Proof of Insertion Sort

Currently I self study CLRS book (Outside of any course, so I got no access to an instructor)

And I am stuck proving Insertion Sort, The proof in CLRS book is not so formal.

Here's the algorithm:

INSERTION-SORT(A)
   for j=2 to A.length (= n)
      key = A[j]
      i = j-1
      while (0<i and key<A[i])
         A[i+1]=A[i]
         i = i-1
      end while
      A[i+1]=key
   end for
end procedure

I tried to formalize the proof with the following pre-post conditions:

Pre-Condition: $A=A_{org}$ and $j=2$ (I.e. $A_{org}$ holds the original values of $A$)

Post-Condition: The array $A$ consists of the same elements as in $A_{org}$ but in a sorted order that is $\forall i_1,i_2\in\{1..n\}, i_1<i_2\to A[i_1]\leq A[i_2]$.

My loop invariant is:

($p$ denotes the $p$'s iteration)

$I(p)="\text{The array $A[1..j-1]$ consists of the same elements as in $A_{org}[1..j-1]$} \land \forall i_1,i_2\in\{1..j-1\}, i_1<i_2\to A[i_1]\leq A[i_2] \land j=2+p"$

Now when I try to prove the inductive step I got stuck and cannot proceed because of the nested $while$ loop and because of the informal sentence "The array $A[1..j-1]$ consists of the same elements as in $A_{org}[1..j-1]$".

Any help on how to prove Insertion Sort rigorously and how to formalize the sentence "The array $A[1..j-1]$ consists of the same elements as in $A_{org}[1..j-1]$" will be appreciated (I want my loop invariant to contain only mathematical symbols and not informal english phrases).

(BTW: I am trying to write the proof in the same style as in Susanna. Epp's Discrete Mathematics book)

Any help will be appreciated. Thanks.

Hint: first prove a loop invariant for the nested while, i.e. you need to prove that the nested while shifts to the right the elements as required to insert the j-element indexed by the outer for loop in its correct place. Then, prove the loop invariant for the outer for loop taking into account the suggestion by @Yuval and you are done.

StackExchange Computer Science Q#32126, answer score: 4