proposition: Theorem minuspf_comp : forall p q r s : list (Term A n), canonical A0 eqA ltM p -> canonical A0 eqA ltM q -> canonical A0 eqA ltM r -> canonical A0 eqA ltM s -> eqP A eqA n p r -> eqP A eqA n q s -> eqP A eqA n (minuspf p q) (minuspf r s).
proof: Proof. Proof using plusA os divA cs. intros p q r s H' H'0 H'1 H'2 H'3 H'4; apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec p (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) q)). apply minuspf_is_pluspf_mults; auto. apply (eqp_trans _ _ _ _ _ _ _ _ _ cs n) with (y := pluspf (A:=A) A0 (eqA:=eqA) plusA eqA_dec (n:=n) (ltM:=ltM) ltM_dec r (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) s)); auto. apply (eqp_sym _ _ _ _ _ _ _ _ _ cs n); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)