proposition: Lemma d_Sm : annotated_recs_d.Sm d.
proof: Proof. rewrite /annotated_recs_d.Sm /annotated_recs_d.precond.Sm /d => n k m ?. rewrite int.zshiftP !alt_sign addrA !(binzS, binSz); [ | lia ..]. rewrite /annotated_recs_d.Sm_cf0_0_0. have b1_pos: 0 < binomialz n m by apply: bin_nonneg; lia. have b2_pos: 0 < binomialz (n + m) m by apply: bin_nonneg; lia. by field; ring_lia. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics shift binomialz rat_of_Z seq_defs