proposition: Lemma refine_size_add n (k' : seqmultinom) (e : T) (p : mpoly n T) (p' : effmpoly T) (q : effmpoly T) : P.Add k' e q p' -> refines Reffmpoly p p' -> refines Rseqmultinom (multinom_of_seqmultinom_val n k') k'.
proof: Proof. move=> Hadd Hp. apply refine_multinom_of_seqmultinom_val. apply (@refine_size_mpoly _ _ _ _ Hp). exists e; move: (Hadd k'); rewrite F.add_eq_o; [|by apply E.eq_refl]. apply M.find_2. Qed.
imports: ZArith NArith FMaps FMapAVL mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice finfun tuple fintype ssralg bigop) CoqEAL(hrel) CoqEAL(refinements) CoqEAL(param binord binnat) CoqEAL(seqmx ) CoqEAL(ssrcomplements) mathcomp.multinomials(mpoly freeg)