proposition: Theorem spec_gcd_gt: forall a b, [a] > [b] -> [gcd_gt a b] = Z.gcd [a] [b].
proof: Proof. intros a b H2. case (spec_digits (gcd_gt a b)); intros H3 H4. case (spec_digits a); intros H5 H6. symmetry; apply Zis_gcd_gcd; auto with zarith. unfold gcd_gt; apply Zspec_gcd_gt_aux with 0; auto with zarith. intros a1 a2; rewrite Z.pow_0_r. case (spec_digits a2); intros H7 H8; intros; apply False_ind; auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen