proposition: Lemma spec_ww_gcd : forall a b, Zis_gcd [[a]] [[b]] [[ww_gcd a b]].
proof: Proof. clear ww_1 spec_ww_1 w_1 spec_w_1. intros a b. change (ww_gcd a b) with (match ww_compare a b with | Gt => ww_gcd_gt a b | Eq => a | Lt => ww_gcd_gt b a end). rewrite spec_ww_compare; case Z.compare_spec; intros Hcmp. Spec_ww_to_Z b;rewrite Hcmp. apply Zis_gcd_for_euclid with 1. ring_simplify ([[b]] - 1 * [[b]]). apply Zis_gcd_0;zarith. apply Zis_gcd_sym;apply spec_ww_gcd_gt;zarith. apply spec_ww_gcd_gt;zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub