proposition: Lemma b'_eq_b_reduction (k : int) : 2 <= k :> int -> b' k = b k -> b' (k + 1) = b (k + 1) -> b' (k + 2) = b (k + 2) -> b' (k + 3) = b (k + 3) -> forall (n : int), n >= k -> b' n = b n.
proof: Proof. move=> kpos ebk0 ebk1 ebk2 ebk3 /= n. pose p : int := n - k; simpl in p. have -> : n = p + k by rewrite /p addrNK. clearbody p; clear n. rewrite lerDr. suff gen (n : int) : 0 <= n -> n <= p -> b' (n + k) = b (n + k). by move=> p_pos; apply: (gen _ p_pos). move: n. elim/int_rect: p => [p h0p hp0 | p ihp n le0n hnp | p _ n hn hp]; last 1 first. - by have := (le_trans hn hp). - have -> : p = 0 by apply/eqP; rewrite eq_le h0p hp0. by rewrite add0r. case: (altP (n =P 0)) => [-> | hn0]. by rewrite add0r. case: (altP (n =P 1)) => [-> | hn1]. by rewrite addrC. case: (altP (n =P 2)) => [-> | hn2]. by rewrite addrC. case: (altP (n =P 3)) => [-> | hn3]. by rewrite addrC. clear ebk0 ebk1 ebk2 ebk3. pose m : int := n - (4 : int); simpl in m. have hm : n = m + 4 by rewrite /m addrK. have le0m : m >= 0 by lia. have hmp : m + 3 <= p by lia. rewrite hm; clearbody m; clear le0n hnp hn0 hn1 hn2 hn3 hm n. have -> : m + 4 + k = int.shift 4 (m + k). by rewrite int.shift2Z addrAC. have b'_Sn4_from2 n : 2 <= n :> int -> annotated_recs_v.P_horner b' n = 0. by move=> hn; apply: b'_Sn4; apply: le_trans hn. have hmk2 : 2 <= m + k :> int by lia. rewrite (Sn4_flat_to_Sn4_rew b'_Sn4_from2 hmk2); clear b'_Sn4_from2. rewrite (Sn4_flat_to_Sn4_rew algo_closures.b_Sn4 hmk2); clear hmk2. rewrite !int.shift2Z ![m + k + _]addrAC. by do 4! (rewrite ihp; [| lia ..]). Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics binomialz shift rat_of_Z seq_defs