proposition: Theorem reduce_mults_invr : forall (Q : list (poly A0 eqA ltM)) (p q : list (Term A n)), reduce Q (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) p) q -> canonical A0 eqA ltM p -> reduce Q p (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) q).
proof: Proof. Proof using plusA os cs. intros Q p q H' H'0. apply reduce_mults_inv_lem with (p := mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) p); auto. Qed.