proposition: Lemma v_SnSk : SnSk v.
proof: Proof. rewrite /SnSk /precond.SnSk. move=> n k ?. rewrite /v. do 1! (rewrite u_SnSk; last by rewrite /annotated_recs_s.precond.SnSk; lia). set u1 := u _ _. set u2 := u _ _. set u3 := u _ _. do 2! (rewrite c_Sn; last by rewrite /c.precond.Sn; lia). do 1! (rewrite c_Sk; last by rewrite /c.precond.Sk; lia). set c1 := c _ _. rewrite /c.Sn_cf0_0 /c.Sk_cf0_0 !int.shift2R. rewrite /annotated_recs_s.SnSk_cf0_0 /annotated_recs_s.SnSk_cf1_0. rewrite /annotated_recs_s.SnSk_cf0_1 /SnSk_cf0_0 /SnSk_cf1_0 /SnSk_cf0_1. by field; ring_lia. Qed.
imports: annotated_recs_v