proposition: Lemma mult_l_correct : forall l la lp, Cond0 PolZ (PhiR l) lp -> PhiR l (mult_l la lp) == 0.
proof: Proof. induction la;simpl;intros. - cring. - destruct lp;trivial. + simpl. cring. + simpl in H;destruct H. rewrite PolZadd_correct. simpl. rewrite PolZmul_correct. simpl. rewrite H. rewrite IHla. * cring. * trivial. Qed.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool Algebra_syntax Ncring Ncring_initial Ncring_tac Integral_domain ZArith Lia