proposition: Lemma sec_poly_bij_rec (l r: seq Party) (m m': Word) (q: {poly Word}): uniq (l ++ r) -> make_shares m' (poly_bij (l ++ r) m m' q) r = make_shares m q r.
proof: Proof. elim: r => [// | a r IHr] in l*. rewrite -cat_rcons -cats1 /= => H. rewrite IHr //. rewrite /make_share sec_poly_bij_part //. by rewrite mem_cat cats1 mem_rcons in_cons eq_refl. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude) extructures(ord fset fmap) Equations(Equations)