proposition: Lemma spec_ww_gcd_gt : forall a b, [[a]] > [[b]] -> Zis_gcd [[a]] [[b]] [[ww_gcd_gt a b]].
proof: Proof. clear ww_1 spec_ww_1 w_1 spec_w_1. intros a b Hgt;unfold ww_gcd_gt. destruct a as [ |ah al]. simpl;apply Zis_gcd_sym;apply Zis_gcd_0. destruct b as [ |bh bl]. simpl;apply Zis_gcd_0. simpl in Hgt. generalize (@spec_eq0 ah);destruct (w_eq0 ah);intros. simpl;rewrite H in Hgt;trivial;rewrite H;trivial;rewrite spec_w_0;simpl. assert ([|bh|] <= 0). apply beta_lex with (d:=[|al|])(b:=[|bl|]) (beta := wB);zarith. Spec_w_to_Z bh;assert ([|bh|] = 0) by zarith. rewrite H1 in Hgt;simpl in Hgt. rewrite H1;simpl;auto. clear H. apply spec_gcd_gt_fix with (n:= 0);trivial. rewrite Z.add_0_r;rewrite spec_ww_digits_. change (2 ^ Zpos (xO w_digits)) with wwB. Spec_ww_to_Z (WW bh bl);zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub