proposition: Lemma v_Sn2 : Sn2 v.
proof: Proof. rewrite /Sn2 /precond.Sn2. move=> n k ?. rewrite /v. do 1! (rewrite u_Sn2; last by rewrite /annotated_recs_s.precond.Sn2; lia). set u1 := u _ _. set u2 := u _ _. set u3 := u _ _. do 3! (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 /Sn2_cf0_0 /Sn2_cf1_0 /Sn2_cf0_1. rewrite /annotated_recs_s.Sn2_cf0_0 /annotated_recs_s.Sn2_cf1_0. rewrite /annotated_recs_s.Sn2_cf0_1. by field; ring_lia. Qed.
imports: annotated_recs_v