proposition: Lemma spec_sgn : forall x, to_Z (sgn x) = Z.sgn (to_Z x).
proof: Proof. intros. unfold sgn. rewrite spec_compare. case Z.compare_spec. rewrite spec_0. intros <-; auto. rewrite spec_0, spec_1. symmetry. rewrite Z.sgn_pos_iff; auto. rewrite spec_0, spec_m1. symmetry. rewrite Z.sgn_neg_iff; auto with zarith. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig