proposition: Theorem spec_inv_normc_bis : forall x : Qc, [inv_norm (of_Qc x)] = /x.
proof: Proof. intros. rewrite <- strong_spec_inv_norm by apply strong_spec_of_Qc_bis. rewrite strong_spec_red. symmetry; apply (Qred_complete (/x)%Q). rewrite spec_inv_norm, ! strong_spec_of_Qc; auto with qarith. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig