proposition: Lemma s_Sn2 : Sn2 s.
proof: Proof. rewrite /Sn2 /precond.Sn2 => n k [ltk0 ltkn]. have Sn2_lcomb_eq_0 : Sn2_lcomb s n k = 0. rewrite /Sn2_lcomb /Sn2_lcomb_cf2 /Sn2_lcomb_cf4. by rewrite -/P1_flat recD1_flat recD1 // -/P3_flat recD3_flat recD3 //; ring. apply/eqP. rewrite -subr_eq0. set nzero := Sn2_lcomb_cf1 n k * d.P1_cf2_0 n k. have nzero_n0 : nzero != 0. by rewrite mulf_eq0 expfz_eq0 /Sn2_lcomb_cf1; ring_lia. rewrite -(mulrI_eq0 _ (lregP nzero_n0)) {nzero_n0}. rewrite -Sn2_lcomb_eq_0. apply/eqP. rewrite /Sn2_cf0_0 /Sn2_cf1_0 /Sn2_cf0_1 /nzero /Sn2_lcomb. rewrite /Sn2_lcomb_cf1 /Sn2_lcomb_cf2 /Sn2_lcomb_cf3 /Sn2_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