proposition: Theorem spec_inv_normc x: [[inv_norm x]] = /[[x]].
proof: Proof. unfold to_Qc. transitivity (Q2Qc (/[x])). unfold Q2Qc. apply Qc_decomp; unfold this. apply Qred_complete; apply spec_inv_norm; auto. unfold Qcinv, Q2Qc. apply Qc_decomp; unfold this. apply Qred_complete. apply Qinv_comp; apply Qeq_sym; apply Qred_correct. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig