proposition: Lemma spec_gcd_cont : forall xh xl yh yl, [[WW xh xl]] > [[WW yh yl]] -> [[WW yh yl]] <= 1 -> Zis_gcd [[WW xh xl]] [[WW yh yl]] [[gcd_cont xh xl yh yl]].
proof: Proof. clear w_0 spec_w_0. intros xh xl yh yl Hgt' Hle. simpl in Hle. assert ([|yh|] = 0). change 1 with (0*wB+1) in Hle. assert (0 <= 1 < wB). split. zarith. apply wB_pos. assert (H1:= beta_lex _ _ _ _ _ Hle (spec_to_Z yl) H). Spec_w_to_Z yh;zarith. unfold gcd_cont; rewrite spec_compare, spec_w_1. case Z.compare_spec; intros Hcmpy. simpl;rewrite H;simpl; rewrite spec_ww_1;rewrite <- Hcmpy;apply Zis_gcd_mod. zarith. rewrite <- (Zmod_unique ([|xh|]*wB+[|xl|]) 1 ([|xh|]*wB+[|xl|]) 0);zarith. rewrite H in Hle; exfalso;zarith. assert (H0 : [|yl|] = 0) by (Spec_w_to_Z yl;zarith). simpl. rewrite H0, H;simpl;apply Zis_gcd_0;trivial. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub