proposition: Theorem spec_gcd: forall a b, to_Z (gcd a b) = Z.gcd (to_Z a) (to_Z b).
proof: Proof. unfold gcd, Z.gcd, to_Z; intros [x | x] [y | y]; rewrite NN.spec_gcd; unfold Z.gcd; auto; case NN.to_Z; simpl; auto with zarith; try rewrite Z.abs_opp; auto; case NN.to_Z; simpl; auto with zarith. Qed.
imports: ZArith Lia BigNumPrelude NSig ZSig