proposition: Lemma d_Sn : annotated_recs_d.Sn d.
proof: Proof. rewrite /annotated_recs_d.Sn /annotated_recs_d.precond.Sn /d => n k m ?. rewrite addrAC !binSz /annotated_recs_d.Sn_cf0_0_0; [ | lia ..]. 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