proposition: Theorem order_minuspf : forall (l1 l2 : list (Term A n)) (a : Term A n), canonical A0 eqA ltM (pX a l1) -> canonical A0 eqA ltM (pX a l2) -> canonical A0 eqA ltM (pX a (minuspf l1 l2)).
proof: Proof. Proof using plusA os divA cs. intros l1 l2 a H' H'0. apply eqp_imp_canonical with (1 := cs) (p := pX a (pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec l1 (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) l2))); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply order_pluspf; auto. apply canonical_pX_eqT with (a := multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) a); auto. change (canonical A0 eqA ltM (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (pX a l2))) in |- *; auto. apply (eqT_sym A n); auto. apply (canonical_nzeroP A A0 eqA n ltM) with (p := l1); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)