proposition: Theorem CombLinear_pluspf : forall (Q : list (poly A0 eqA ltM)) (p : list (Term A n)), CombLinear Q p -> forall q : list (Term A n), CombLinear Q q -> CombLinear Q (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec p q).
proof: Proof. Proof using os minusA invA divA cs A1. intros Q p H'; elim H'; auto. intros q H'0. cut (canonical A0 eqA ltM q); [ intros Op1 | apply CombLinear_canonical with (Q := Q); auto ]. apply CombLinear_comp with (p := q); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (pO A n) q); auto; apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. intros a p0 q s H'0 H'1 H'2 H'3 H'4 q0 H'5. cut (canonical A0 eqA ltM q); [ intros C0 | apply inPolySet_imp_canonical with (L := Q); auto ]. cut (canonical A0 eqA ltM q0); [ intros Op1 | apply CombLinear_canonical with (Q := Q); auto ]. cut (canonical A0 eqA ltM p0); [ intros Op2 | apply CombLinear_canonical with (Q := Q); auto ]. apply CombLinear_1 with (a := a) (p := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec p0 q0) (q := q); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec (mults (A:=A) multA (n:=n) a q) p0) q0); auto. apply eqp_pluspf_com with (1 := cs); auto. 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. Qed.