normcV available with real-closed.1.1.3

[affeldt-aist]

Note that the lemma

Lemma normcV x : normc x^-1 = (normc x)^-1.

is now available with real-closed.1.1.3 as Normc.normcV.

See math-comp/real-closed#35.

fyi @ybertot