proposition: Lemma c_Sk : annotated_recs_c.Sk c.
proof: Proof. rewrite /annotated_recs_c.Sk /annotated_recs_c.precond.Sk /c => n k ?. rewrite int.zshiftP addrA !(binSz, binzS); [ | lia ..]. rewrite /annotated_recs_c.Sk_cf0_0. by field; ring_lia. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics shift binomialz rat_of_Z seq_defs