proposition: Lemma reduceplus_mults_invr_lem : forall (Q : list (poly A0 eqA ltM)) (p q : list (Term A n)), reduceplus Q p q -> forall r : list (Term A n), eqP A eqA n p (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) r) -> canonical A0 eqA ltM r -> reduceplus Q r (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'; elim H'; auto. intros x y H'0 r H'1 H'2. apply Rstar_0; auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) x); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) r)); auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := mults (A:=A) multA (n:=n) (multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (invTerm (A:=A) invA (n:=n) (T1 A1 n))) r); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := mults (A:=A) multA (n:=n) (T1 A1 n) r); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. intros x y z H'0 H'1 H'2 r H'3 H'4. apply Rstar_n with (y := mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) y); auto. apply reduce_mults_invr with (1 := cs); auto. apply reduce_eqp_com with (1 := cs) (p := x) (q := y); auto. apply eqp_imp_canonical with (p := mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) r) (1 := cs); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply reduceplus_mults; auto. apply canonical_reduce with (1 := cs) (3 := H'0); auto. apply eqp_imp_canonical with (p := mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) r) (1 := cs); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.