proposition: Lemma Sn4_flat_to_Sn4_rew (w : int -> rat) : (forall n : int, 2 <= n :> int -> annotated_recs_v.P_horner w n = 0) -> (forall n : int, 2 <= n :> int -> w (int.shift 4 n) = - (annotated_recs_v.P_cf0 n * w n + annotated_recs_v.P_cf1 n * w (int.shift 1 n) + annotated_recs_v.P_cf2 n * w (int.shift 2 n) + annotated_recs_v.P_cf3 n * w (int.shift 3 n)) / annotated_recs_v.P_cf4 n).
proof: Proof. move=> horner_hyp n le_2_n. have le_0_n : n >= 0 by apply: (le_trans _ le_2_n). set goal := (_ = _). move: {horner_hyp} (horner_hyp n le_2_n). rewrite /annotated_recs_v.P_horner /punk.horner_seqop /=. set t0 := (X in _ + X = 0). set t1 := (X in _ + X + t0 = 0). set t2 := (X in _ + X + t1 + t0 = 0). set t3 := (X in _ + X + t2 + t1 + t0 = 0). set t4 := (X in X + t3 + t2 + t1 + t0 = 0). move=> horner_hyp. rewrite {}/goal -{1}/t0 -{1}/t1 -{1}/t2 -{1}/t3. move: @t4 horner_hyp => /=. set c4 := annotated_recs_v.P_cf4 n => hyp. clearbody t0 t1 t2 t3. have c4_neq_0 : c4 != 0. rewrite /c4 /annotated_recs_v.P_cf4. apply: mulf_neq0; last by ring_lia. apply: mulf_neq0; first by ring_lia. apply: lt0r_neq0; apply: addr_gt0; last by ring_lia. apply: addr_gt0; last by ring_lia. apply: addr_gt0; last by ring_lia. by apply: addr_gt0; ring_lia. clearbody c4. clear le_0_n. rewrite mulNr. apply/eqP. rewrite -addr_eq0. have <- : (c4 * (w (int.shift 4 n) + (t0 + t1 + t2 + t3) / c4) == 0) = (w (int.shift 4 n) + (t0 + t1 + t2 + t3) / c4 == 0). by apply: mulrI_eq0; first by apply/lregP. rewrite mulrDr [c4 * (_ / c4)]mulrC. rewrite -{}hyp 3!(int.shiftS n). apply/eqP. by field. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics binomialz shift rat_of_Z seq_defs