proposition: Lemma s_SnSk : SnSk s.
proof: Proof. rewrite /SnSk /precond.SnSk => n k [ltk0 ltkn]. have SnSk_lcomb_eq_0 : SnSk_lcomb s n k = 0. rewrite /SnSk_lcomb /SnSk_lcomb_cf1 /SnSk_lcomb_cf2 /SnSk_lcomb_cf3. by rewrite /SnSk_lcomb_cf4 -/P3_flat recD3_flat recD3 //; ring. apply/eqP. rewrite -subr_eq0. set nzero := d.P3_cf1_1 n k. have nzero_n0 : nzero != 0 by rewrite /nzero /d.P3_cf1_1; ring_lia. rewrite -(mulrI_eq0 _ (lregP nzero_n0)) // {nzero_n0}. rewrite -SnSk_lcomb_eq_0. apply/eqP. rewrite /SnSk_cf0_0 /SnSk_cf1_0 /SnSk_cf0_1 /nzero /SnSk_lcomb. rewrite /SnSk_lcomb_cf1 /SnSk_lcomb_cf2 /SnSk_lcomb_cf3 /SnSk_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