proposition: Theorem term_inv_iter_enough : ∀ a i j k, k ≤ i → k ≤ j → (term_inv i a k = term_inv j a k)%K.
proof: Proof. intros a i j k Hki Hkj. revert j k Hki Hkj. induction i; intros. apply Nat.le_0_r in Hki; subst k. destruct j; reflexivity. simpl. destruct k; simpl. destruct j; reflexivity. destruct j. apply Nat.nle_succ_0 in Hkj; contradiction. simpl. apply rng_mul_compat_l. apply summation_compat; intros l (Hl, Hlj). apply rng_mul_compat_l. destruct l. rewrite Nat.sub_0_r. apply IHi; apply Nat.succ_le_mono; assumption. apply IHi; [ fast_omega Hki | fast_omega Hkj ]. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation