proposition: Lemma size_update_anti_literals p k st : size (update_anti_literals p k st) = size st.
proof: Proof. rewrite -(size_map ((fun '(y, _) => let '(_, p) := y in p))) -[map _ _]/(spos _). by rewrite (perm_size (perm_spos_update_anti_literals _ _ _)) size_map. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)