proposition: Theorem Rminus_is_reduceplus : forall (Q : list (poly A0 eqA ltM)) (a : Term A n) (q : list (Term A n)) (nZa : ~ zeroP (A:=A) A0 eqA (n:=n) a), canonical A0 eqA ltM q -> inPolySet A A0 eqA n ltM (pX a q) Q -> forall r : list (Term A n), canonical A0 eqA ltM r -> divPp a r -> forall p : list (Term A n), canonical A0 eqA ltM p -> incl r p -> reduceplus A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec Q p (Rminus a nZa p (pX a q) r).
proof: Proof. Proof using plusA os cs. intros Q a q nZa Op0 in0 r; elim r; clear r. simpl in |- *; intros H' H'0 p H'1 H'2; auto. apply Rstar_0; auto. intros a0 r1 Rec Op1 divp0 p Op2 incl0. cut (canonical A0 eqA ltM r1); [ intros Cr1 | apply canonical_imp_canonical with (a := a0); auto ]. cut (canonical A0 eqA ltM (pX a q)); [ intros Caq | apply inPolySet_imp_canonical with (L := Q); auto ]. elim divp0; intros H' H'0; clear divp0. apply reduceplus_trans with (1 := cs) (y := Rminus a nZa p (pX a q) r1); auto. apply Rec; auto. red in |- *; intros p' H; apply incl0; auto with datatypes. apply reduceplus_eqp_com with (1 := cs) (p := Rminus a nZa p (pX a q) r1) (q := minuspf A A0 A1 eqA invA minusA multA eqA_dec n ltM ltM_dec (Rminus a nZa p (pX a q) r1) (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) a0 (b:=a) nZa) (pX a q))); auto. apply reduce_imp_reduceplus with (1 := cs); auto. apply minus_is_reduce; auto. apply Rminus_in; auto with datatypes. Qed.