proposition: Theorem CombLinear_canonical : forall (Q : list (poly A0 eqA ltM)) (p : list (Term A n)), CombLinear Q p -> canonical A0 eqA ltM p.
proof: Proof. Proof using os minusA invA divA cs A1. intros Q p H'; elim H'; auto. intros a p0 q s H'0 H'1 H'2 H'3 H'4. apply eqp_imp_canonical 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) (1 := cs); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply canonical_pluspf; auto. apply canonical_mults with (1 := cs); auto. apply inPolySet_imp_canonical with (L := Q); auto. Qed.