proposition: Lemma s_Sk2 : Sk2 s.
proof: Proof. rewrite /Sk2 /precond.Sk2 => n k [ltk0 ltSkn]. have Sk2_lcomb_eq_0 : Sk2_lcomb s n k = 0. rewrite /Sk2_lcomb /Sk2_lcomb_cf1 /Sk2_lcomb_cf2 /Sk2_lcomb_cf3. by rewrite /Sk2_lcomb_cf4 -/P4_flat recD4_flat recD4 //; ring. apply/eqP. rewrite -subr_eq0. set nzero := d.P4_cf0_2 n k. have nzero_n0 : nzero != 0 by rewrite /nzero /d.P4_cf0_2 !mulf_eq0; ring_lia. rewrite -(mulrI_eq0 _ (lregP nzero_n0)) // {nzero_n0}. rewrite -Sk2_lcomb_eq_0. apply/eqP. rewrite /Sk2_cf0_0 /Sk2_cf0_1 /nzero /Sk2_lcomb. rewrite /Sk2_lcomb_cf1 /Sk2_lcomb_cf2 /Sk2_lcomb_cf3 /Sk2_lcomb_cf4. rewrite /d.P1_flat /d.P2_flat /d.P3_flat /d.P4_flat. rewrite /d.P1_cf0_0 /d.P1_cf0_1 /d.P1_cf1_0 /d.P1_cf1_1 /d.P1_cf2_0 /d.P2_cf0_0 /d.P2_cf1_0 /d.P2_cf2_0 /d.P2_cf3_0 /d.P3_cf0_0 /d.P3_cf0_1 /d.P3_cf1_0 /d.P3_cf1_1 /d.P4_cf0_0 /d.P4_cf0_1 /d.P4_cf0_2. by field; ring_lia. Qed.
imports: annotated_recs_s