proposition: Theorem Rminus_in : forall (r p q : list (Term A n)) (a b : Term A n) (nZb : ~ zeroP (A:=A) A0 eqA (n:=n) b), divPp b r -> In a p -> canonical A0 eqA ltM p -> canonical A0 eqA ltM (pX b q) -> canonical A0 eqA ltM (pX a r) -> In a (Rminus b nZb p (pX b q) r).
proof: Proof. Proof using plusA os cs. intros r; elim r; simpl in |- *; auto. intros a l H' p q a0 b nZb H'0 H'1 H'2 H'3 H'4. cut (~ zeroP (A:=A) A0 eqA (n:=n) b); [ intros Z1 | apply canonical_nzeroP with (ltM := ltM) (p := q); auto ]. elim H'0; intros H'6 H'7; clear H'0. apply minuspf_in; auto. apply H'; auto. apply canonical_skip_fst with (b := a); auto. apply eqT_compat_ltTl with (b := a); auto. apply (eqTerm_imp_eqT A eqA n); auto. inversion H'6; auto. apply (canonical_pX_order A A0 eqA) with (l := l); auto. apply canonical_Rminus; auto. apply canonical_imp_canonical with (a := a); auto. apply canonical_imp_canonical with (a := a0); auto. change (canonical A0 eqA ltM (mults (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) a (b:=b) nZb) (pX b q))) in |- *; auto. Qed.