proposition: Lemma u_Sk2 : s.Sk2 u.
proof: Proof. have ? := z_ann. rewrite /s.Sk2 /s.precond.Sk2. move => n k ?. rewrite /u. rewrite s_Sk2 //. set s1 := s _ _. set s2 := s _ _. set z1 := z _. rewrite /s.Sk2_cf0_0 /s.Sk2_cf0_1. by field; ring_lia. Qed.