proposition: Theorem spec_inv : forall x, [inv x] == /[x].
proof: Proof. destruct x as [ z | n d ]. simpl. rewrite ZZ.spec_compare; destr_zcompare. rewrite <- H. simpl; nzsimpl; compute; auto. simpl. destr_eqb; nzsimpl; [ intros; rewrite Z.abs_eq in *; lia | intros _ ]. set (z':=ZZ.to_Z z) in *; clearbody z'. red; simpl. rewrite Z.abs_eq by lia. rewrite Z2Pos.id by auto. unfold Qinv; simpl; destruct z'; simpl; auto; discriminate. simpl. destr_eqb; nzsimpl; [ intros; rewrite Z.abs_neq in *; lia | intros _ ]. set (z':=ZZ.to_Z z) in *; clearbody z'. red; simpl. rewrite Z.abs_neq by lia. rewrite Z2Pos.id by lia. unfold Qinv; simpl; destruct z'; simpl; auto; discriminate. simpl. rewrite ZZ.spec_compare; destr_zcompare. rewrite <- H. simpl; nzsimpl. destr_eqb; intros; compute; auto. simpl. destr_eqb; nzsimpl; intros. intros; rewrite Z.abs_eq in *; lia. intros; rewrite Z.abs_eq in *; lia. nsubst; compute; auto. set (n':=ZZ.to_Z n) in *; clearbody n'. rewrite Z.abs_eq by lia. red; simpl. rewrite Z2Pos.id by auto. unfold Qinv; simpl; destruct n'; simpl; auto; try discriminate. rewrite Pos2Z.inj_mul, Z2Pos.id; auto. simpl. destr_eqb; nzsimpl; intros. intros; rewrite Z.abs_neq in *; lia. intros; rewrite Z.abs_neq in *; lia. nsubst; compute; auto. set (n':=ZZ.to_Z n) in *; clearbody n'. red; simpl; nzsimpl. rewrite Z.abs_neq by lia. rewrite Z2Pos.id by lia. unfold Qinv; simpl; destruct n'; simpl; auto; try discriminate. assert (T : forall x, Zneg x = Z.opp (Zpos x)) by auto. rewrite T, Pos2Z.inj_mul, Z2Pos.id; auto; ring. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig