proposition: Lemma size_lagrange_poly_part {R: fieldType} l (m: R * R) r: (size (\sum_(j <- subseqs_rec l m r) lagrange_poly_part j)%R <= size (l ++ m :: r))%N.
proof: Proof. generalize dependent m. generalize dependent l. elim: r => /= [|m' r IHr] l m. 1: { rewrite big_seq1 size_cat addn1. apply: leq_trans. 1: by apply: size_scale_leq. apply: leq_trans. - by apply: size_lagrange_basis. - by rewrite /unzip1 size_map ltnSn. } rewrite big_cons. apply: leq_trans. 1: by apply: size_add. rewrite geq_max. apply /andP. split. - rewrite /lagrange_poly_part /=. apply: leq_trans. 1: by apply: size_scale_leq. replace (size (l ++ [:: m, m' & r])) with (size (unzip1 (l ++ [:: m' & r]))).+1. 1: by apply: size_lagrange_basis. by rewrite /unzip1 size_map !size_cat -addnS. - replace (size (l ++ [:: m, m' & r])) with (size ((l ++ [:: m]) ++ m' :: r)). 1: by apply: IHr. by rewrite !size_cat addn1 !addnS. 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)