proposition: Lemma v_Sk2 : Sk2 v.
proof: Proof. rewrite /Sk2 /precond.Sk2. move=> n k ?. rewrite /v. do 1! (rewrite u_Sk2; last by rewrite /annotated_recs_s.precond.Sk2; lia). set u1 := u _ _. set u2 := u _ _. do 3! (rewrite c_Sk; last by rewrite /c.precond.Sk; lia). set c1 := c _ _. rewrite /c.Sk_cf0_0 /annotated_recs_s.Sk2_cf0_0 /annotated_recs_s.Sk2_cf0_1 /Sk2_cf0_0 /Sk2_cf0_1 !int.shift2R. by field; ring_lia. Qed.
imports: annotated_recs_v