proposition: Lemma c_Sn : annotated_recs_c.Sn c.
proof: Proof. rewrite /annotated_recs_c.Sn /annotated_recs_c.precond.Sn /c => n k ?. rewrite addrAC !binSz /annotated_recs_c.Sn_cf0_0; [| lia..]. by field; ring_lia. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics shift binomialz rat_of_Z seq_defs