proposition: Theorem CombLinear_id : forall (Q : list (poly A0 eqA ltM)) (p : list (Term A n)), inPolySet A A0 eqA n ltM p Q -> CombLinear Q p.
proof: Proof. Proof using os minusA invA divA cs A1. intros Q p H'. cut (canonical A0 eqA ltM p); [ intros C0 | apply inPolySet_imp_canonical with (L := Q); auto ]. 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) (T1 A1 n) p) (pO A n)); auto. apply CombLinear_1 with (a := T1 A1 n) (p := pO A n) (q := p); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := mults (A:=A) multA (n:=n) (T1 A1 n) p); auto. Qed.