proposition: Theorem spec_compare : forall x y, compare x y = Z.compare (to_Z x) (to_Z y).
proof: Proof. unfold compare, to_Z. destruct x as [x|x], y as [y|y]; rewrite ?NN.spec_compare, ?NN.spec_0, ?Z.compare_opp; auto; assert (Hx:=NN.spec_pos x); assert (Hy:=NN.spec_pos y); set (X:=NN.to_Z x) in *; set (Y:=NN.to_Z y) in *; clearbody X Y. - destruct (Z.compare_spec X 0) as [EQ|LT|GT]. + rewrite <- Z.opp_0 in EQ. now rewrite EQ, Z.compare_opp. + exfalso. lia. + symmetry. change (X > -Y). lia. - destruct (Z.compare_spec 0 X) as [EQ|LT|GT]. + rewrite <- EQ, Z.opp_0; auto. + symmetry. change (-X < Y). lia. + exfalso. lia. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig