proposition: Lemma spec_ww_gcd_gt_aux : forall p cont n, (forall xh xl yh yl, [[WW xh xl]] > [[WW yh yl]] -> [[WW yh yl]] <= 2^n -> Zis_gcd [[WW xh xl]] [[WW yh yl]] [[cont xh xl yh yl]]) -> forall ah al bh bl , [[WW ah al]] > [[WW bh bl]] -> [[WW bh bl]] <= 2^(Zpos p + n) -> Zis_gcd [[WW ah al]] [[WW bh bl]] [[ww_gcd_gt_aux p cont ah al bh bl]].
proof: Proof. induction p;intros cont n Hcont ah al bh bl Hgt Hs;simpl ww_gcd_gt_aux. assert (0 < Zpos p). unfold Z.lt;reflexivity. apply spec_ww_gcd_gt_aux_body with (n := Zpos (xI p) + n); trivial;rewrite Pos2Z.inj_xI. intros. apply IHp with (n := Zpos p + n). 2: zarith. intros. apply IHp with (n := n );zarith. apply Z.le_trans with (2 ^ (2* Zpos p + 1+ n -1)). zarith. apply Z.pow_le_mono_r;zarith. assert (0 < Zpos p). unfold Z.lt;reflexivity. apply spec_ww_gcd_gt_aux_body with (n := Zpos (xO p) + n );trivial. rewrite (Pos2Z.inj_xO p). intros. apply IHp with (n := Zpos p + n - 1). 2: zarith. intros. apply IHp with (n := n -1 ). 2: zarith. intros;apply Hcont. zarith. apply Z.le_trans with (2^(n-1)). zarith. apply Z.pow_le_mono_r;zarith. apply Z.le_trans with (2 ^ (Zpos p + n -1)). zarith. apply Z.pow_le_mono_r;zarith. apply Z.le_trans with (2 ^ (2*Zpos p + n -1)). zarith. apply Z.pow_le_mono_r;zarith. apply spec_ww_gcd_gt_aux_body with (n := n+1);trivial. rewrite Z.add_comm;trivial. ring_simplify (n + 1 - 1);trivial. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub