proposition: Lemma compute_list_correct : forall l lla lp, Cond0 PolZ (PhiR l) lp -> Cond0 PolZ (PhiR l) (compute_list lla lp).
proof: Proof. induction lla;simpl;intros;trivial. apply IHlla;simpl;split;trivial. apply mult_l_correct;trivial. Qed.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool Algebra_syntax Ncring Ncring_initial Ncring_tac Integral_domain ZArith Lia