proposition: Theorem spec_gcd: forall a b, [gcd a b] = Z.gcd [a] [b].
proof: Proof. intros a b. case (spec_digits a); intros H1 H2. case (spec_digits b); intros H3 H4. unfold gcd. rewrite spec_compare. case Z.compare_spec. intros HH; rewrite HH; symmetry; apply Zis_gcd_gcd; auto. apply Zis_gcd_refl. intros; transitivity (Z.gcd [b] [a]). apply spec_gcd_gt; auto with zarith. apply Zis_gcd_gcd; auto with zarith. apply Z.gcd_nonneg. apply Zis_gcd_sym; apply Zgcd_is_gcd. intros; apply spec_gcd_gt; auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen