proposition: Theorem CombLinear_minuspf : 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 (minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec p q).
proof: Proof. Proof using os divA cs. intros Q p H' q H'0; try assumption. cut (canonical A0 eqA ltM p); [ intros Op1 | apply CombLinear_canonical with (Q := Q); auto ]. cut (canonical A0 eqA ltM q); [ intros Op2 | apply CombLinear_canonical with (Q := Q); auto ]. apply CombLinear_comp with (p := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec p (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) q)); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.