proposition: Theorem sequence_gcd_divide : ∀ s g m i, (∀ j, m ≤ j → sequence_gcd_upto s j = g) → (g | s i).
proof: Proof. intros s g m i H. destruct (le_dec m i) as [H1| H1]. rewrite <- (H i H1). destruct i; [ apply Nat.divide_refl | apply Nat.gcd_divide_l ]. apply Nat.nle_gt in H1. rewrite <- (H m (Nat.le_refl m)). remember (m - i)%nat as k eqn:Hk. assert (H2 : m = (i + k)%nat). rewrite Hk, Nat.add_comm. rewrite Nat.sub_add; [ apply eq_refl | apply Nat.lt_le_incl, H1 ]. subst m; clear H H1 Hk. revert i. induction k; intros. rewrite Nat.add_0_r. induction i; [ apply Nat.divide_refl | apply Nat.gcd_divide_l ]. rewrite Nat.add_succ_r; simpl. eapply Nat.divide_trans; [ apply Nat.gcd_divide_r | apply IHk ]. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series