proposition: Lemma d_Sk : annotated_recs_d.Sk d.
proof: Proof. rewrite /annotated_recs_d.Sk /annotated_recs_d.precond.Sk => n k m ?. by rewrite /annotated_recs_d.Sk_cf0_0_0 rat_of_ZEdef mul1r. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics shift binomialz rat_of_Z seq_defs