proposition: Theorem Zspec_gcd_gt_aux: forall p n a b cont, [a] > [b] -> [a] < 2 ^ (Zpos p + n) -> (forall a1 b1, [a1] < 2 ^ n -> [a1] > [b1] -> Zis_gcd [a1] [b1] [cont a1 b1]) -> Zis_gcd [a] [b] [gcd_gt_aux p cont a b].
proof: Proof. intros p; elim p; clear p. intros p Hrec n a b cont H2 H3 H4. unfold gcd_gt_aux; apply Zspec_gcd_gt_body with (Zpos (xI p) + n); auto. intros a1 b1 H6 H7. apply Hrec with (Zpos p + n); auto. replace (Zpos p + (Zpos p + n)) with (Zpos (xI p) + n - 1); auto. rewrite Pos2Z.inj_xI; ring. intros a2 b2 H9 H10. apply Hrec with n; auto. intros p Hrec n a b cont H2 H3 H4. unfold gcd_gt_aux; apply Zspec_gcd_gt_body with (Zpos (xO p) + n); auto. intros a1 b1 H6 H7. apply Hrec with (Zpos p + n - 1); auto. replace (Zpos p + (Zpos p + n - 1)) with (Zpos (xO p) + n - 1); auto. rewrite Pos2Z.inj_xO; ring. intros a2 b2 H9 H10. apply Hrec with (n - 1); auto. replace (Zpos p + (n - 1)) with (Zpos p + n - 1); auto with zarith. intros a3 b3 H12 H13; apply H4; auto with zarith. apply Z.lt_le_trans with (1 := H12). apply Z.pow_le_mono_r; auto with zarith. intros n a b cont H H2 H3. simpl gcd_gt_aux. apply Zspec_gcd_gt_body with (n + 1); auto with zarith. rewrite Z.add_comm; auto. intros a1 b1 H5 H6; apply H3; auto. replace n with (n + 1 - 1); auto; try ring. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen