proposition: Lemma b_Sn2 (n : int) : n >= 0 -> annotated_recs_c.P_horner b n = 0.
proof: Proof. move=> hn. case: (altP (n =P 0)) => [-> | h0]; first exact: b_Sn2_at_0. case: (altP (n =P 1)) => [-> | h1]; first exact: b_Sn2_at_1. pose p : int := n - (2 : int); simpl in p. have hnp : n = p + (2 : int) by rewrite /p addrNK. have {hn h0 h1} le0p : 0 <= p by lia. have {le0p hnp p} h : (2 : int) <= n by rewrite hnp lerDr. exact: b_Sn2_almost. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) tactics binomialz shift rat_of_Z seq_defs