proposition: Theorem reduceplus_mults_inv : forall a : Term A n, ~ zeroP (A:=A) A0 eqA (n:=n) a -> eqT a (T1 A1 n) -> forall (Q : list (poly A0 eqA ltM)) (p q : list (Term A n)), reduceplus Q (mults (A:=A) multA (n:=n) a p) (mults (A:=A) multA (n:=n) a q) -> canonical A0 eqA ltM p -> reduceplus Q p q.
proof: Proof. Proof using plusA os cs. intros a H' H'0 Q p q H'1 H'2. apply reduceplus_mults_invf0 with (a := a) (p := mults (A:=A) multA (n:=n) a p) (q := mults (A:=A) multA (n:=n) a q); auto. Qed.