proposition: Theorem Zspec_gcd_gt_body: forall a b cont p, [a] > [b] -> [a] < 2 ^ p -> (forall a1 b1, [a1] < 2 ^ (p - 1) -> [a1] > [b1] -> Zis_gcd [a1] [b1] [cont a1 b1]) -> Zis_gcd [a] [b] [gcd_gt_body a b cont].
proof: Proof. intros a b cont p H2 H3 H4; unfold gcd_gt_body. rewrite ! spec_compare, spec_0. case Z.compare_spec. intros ->; apply Zis_gcd_0. intros HH; absurd (0 <= [b]); auto with zarith. case (spec_digits b); auto with zarith. intros H5; case Z.compare_spec. intros H6; rewrite <- (Z.mul_1_r [b]). rewrite (Z_div_mod_eq_full [a] [b]); auto with zarith. rewrite <- spec_mod_gt; auto with zarith. rewrite H6; rewrite Z.add_0_r. apply Zis_gcd_mult; apply Zis_gcd_1. intros; apply False_ind. case (spec_digits (mod_gt a b)); auto with zarith. intros H6; apply DoubleDiv.Zis_gcd_mod; auto with zarith. apply DoubleDiv.Zis_gcd_mod; auto with zarith. rewrite <- spec_mod_gt; auto with zarith. assert (F2: [b] > [mod_gt a b]). case (Z_mod_lt [a] [b]); auto with zarith. repeat rewrite <- spec_mod_gt; auto with zarith. assert (F3: [mod_gt a b] > [mod_gt b (mod_gt a b)]). case (Z_mod_lt [b] [mod_gt a b]); auto with zarith. rewrite <- spec_mod_gt; auto with zarith. repeat rewrite <- spec_mod_gt; auto with zarith. apply H4; auto with zarith. apply Z.mul_lt_mono_pos_r with 2; auto with zarith. apply Z.le_lt_trans with ([b] + [mod_gt a b]); auto with zarith. apply Z.le_lt_trans with (([a]/[b]) * [b] + [mod_gt a b]); auto with zarith. - apply Z.add_le_mono_r. rewrite <- (Z.mul_1_l [b]) at 1. apply Z.mul_le_mono_nonneg_r; auto with zarith. change 1 with (Z.succ 0). apply Z.le_succ_l. apply Z.div_str_pos; auto with zarith. - rewrite Z.mul_comm; rewrite spec_mod_gt; auto with zarith. rewrite <- Z_div_mod_eq_full; auto with zarith. rewrite Z.mul_comm, <- Z.pow_succ_r, Z.sub_1_r, Z.succ_pred; auto. apply Z.le_0_sub. change 1 with (Z.succ 0). apply Z.le_succ_l. destruct p; simpl in H3; auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen