proposition: Theorem spec_inv_norm : forall x, [inv_norm x] == /[x].
proof: Proof. intros. rewrite <- spec_inv. destruct x as [ z | n d ]. simpl. rewrite ZZ.spec_compare; destr_zcompare; auto with qarith. simpl; nzsimpl; destr_eqb. destr_zcompare; simpl; auto with qarith. destr_eqb; nzsimpl; auto with qarith. intros _ Hd; rewrite Hd; auto with qarith. destr_eqb; nzsimpl; auto with qarith. intros _ Hd; rewrite Hd; auto with qarith. destr_zcompare; auto with qarith. destr_zcompare; nzsimpl; simpl; auto with qarith; intros. destr_eqb; nzsimpl; [ intros; rewrite Z.abs_eq in *; lia | intros _ ]. rewrite H0; auto with qarith. lia. destr_zcompare; nzsimpl; simpl; auto with qarith. destr_eqb; nzsimpl; [ intros; rewrite Z.abs_neq in *; lia | intros _ ]. rewrite H0; auto with qarith. lia. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig