proposition: Lemma bij_poly_bij (U: seq Party) (m m': Word) (q: {poly Word}): uniq U -> poly_bij U m' m (poly_bij U m m' q) = q.
proof: Proof. move=> Huniq. rewrite {1}/poly_bij. rewrite sec_poly_bij //. rewrite /poly_bij. rewrite !lagrange_sub_zero_cons. 2,3: by rewrite /= no_zero_share uniq_make_shares. rewrite -GRing.addrA -tail_poly_add. rewrite (make_shares_same_x m' m). rewrite lagrange_add_zero_cons. 2: by rewrite /= no_zero_share uniq_make_shares. rewrite -GRing.opprB GRing.addNr. rewrite /zero_points -map_cons -/(zero_points _). rewrite lagrange_zero. 2: by rewrite /= no_zero_share uniq_make_shares. by rewrite /tail_poly polyseq0 GRing.addr0. 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)