proposition: Lemma u_Sn2 : s.Sn2 u.
proof: Proof. rewrite /s.Sn2 /s.precond.Sn2. move => n k ?. rewrite /u. rewrite z_Sn2; last by rewrite /z.precond.Sn2; lia. rewrite s_Sn2 //. set s1 := s _ _. set s2 := s _ _. set s3 := s _ _. set z1 := z _. set z2 := z _. rewrite /z.Sn2_cf0 /z.Sn2_cf1 /s.Sn2_cf0_0 /s.Sn2_cf1_0 /s.Sn2_cf0_1. by field; ring_lia. Qed.