proposition: Theorem CombLinear_compo : forall (p : list (Term A n)) (L1 : list (poly A0 eqA ltM)), CombLinear L1 p -> forall L2 : list (poly A0 eqA ltM), (forall q : list (Term A n), inPolySet A A0 eqA n ltM q L1 -> CombLinear L2 q) -> CombLinear L2 p.
proof: Proof. Proof using os minusA invA divA cs A1. intros p L1 H'; elim H'; auto. intros a p0 q s H'0 H'1 H'2 H'3 H'4 L2 H'5. apply CombLinear_comp with (p := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a q) p0); auto. apply eqp_imp_canonical with (1 := cs) (p := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a q) p0); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply canonical_pluspf; auto. apply canonical_mults with (1 := cs); auto. apply inPolySet_imp_canonical with (L := L1); auto. apply CombLinear_canonical with (1 := H'2); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.