proposition: Lemma interp_PElist_ok : forall l lpe, interp_PElist l lpe -> MPcond (mk_monpol_list lpe) l.
proof: Proof. intros l lpe; induction lpe as [|a lpe IHlpe];simpl. - trivial. - destruct a as [p p0];simpl;intros H. assert (HH:=mon_of_pol_ok (norm_subst 0 nil p)); destruct (mon_of_pol (norm_subst 0 nil p)). + split. * rewrite <- norm_subst_spec by exact I. destruct lpe;try destruct H as [H H0];rewrite <- H; rewrite (norm_subst_spec 0 nil); try exact I;apply HH;trivial. * apply IHlpe. destruct lpe;simpl;trivial. destruct H as [H H0]. exact H0. + apply IHlpe. destruct lpe;simpl;trivial. destruct H as [H H0]. exact H0. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory