proposition: Lemma u_SnSk : s.SnSk u.
proof: Proof. have ? := z_ann. rewrite /s.SnSk /s.precond.SnSk. move => n k ?. rewrite /u. rewrite s_SnSk //. set s1 := s _ _. set s2 := s _ _. set s3 := s _ _. set z1 := z _. set z2 := z _. rewrite /s.SnSk_cf0_0 /s.SnSk_cf1_0 /s.SnSk_cf0_1. by field; ring_lia. Qed.